%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM378+1.015.020 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:13:34 PM UTC 2026
% Result : Unsatisfiable 45.24s 7.39s
% Output : Refutation 46.22s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81,X82,X83,X84,X85,X86,X87,X88,X89,X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100,X101,X102,X103,X104,X105,X106,X107,X108,X109,X110,X111,X112,X113,X114,X115,X116,X117,X118,X119,X120,X121] :
( 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) = n11
& succ(n11) = n12
& succ(n12) = n13
& succ(n13) = n14
& succ(n14) = n15
& succ(n15) = n0
& pred(n0) = n15
& 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
& pred(n11) = n10
& pred(n12) = n11
& pred(n13) = n12
& pred(n14) = n13
& pred(n15) = n14
& 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(n0,n11) = n11
& sum(n0,n12) = n12
& sum(n0,n13) = n13
& sum(n0,n14) = n14
& sum(n0,n15) = n15
& 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) = n11
& sum(n1,n11) = n12
& sum(n1,n12) = n13
& sum(n1,n13) = n14
& sum(n1,n14) = n15
& sum(n1,n15) = 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) = n11
& sum(n2,n10) = n12
& sum(n2,n11) = n13
& sum(n2,n12) = n14
& sum(n2,n13) = n15
& sum(n2,n14) = n0
& sum(n2,n15) = 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) = n11
& sum(n3,n9) = n12
& sum(n3,n10) = n13
& sum(n3,n11) = n14
& sum(n3,n12) = n15
& sum(n3,n13) = n0
& sum(n3,n14) = n1
& sum(n3,n15) = 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) = n11
& sum(n4,n8) = n12
& sum(n4,n9) = n13
& sum(n4,n10) = n14
& sum(n4,n11) = n15
& sum(n4,n12) = n0
& sum(n4,n13) = n1
& sum(n4,n14) = n2
& sum(n4,n15) = 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) = n11
& sum(n5,n7) = n12
& sum(n5,n8) = n13
& sum(n5,n9) = n14
& sum(n5,n10) = n15
& sum(n5,n11) = n0
& sum(n5,n12) = n1
& sum(n5,n13) = n2
& sum(n5,n14) = n3
& sum(n5,n15) = n4
& sum(n6,n0) = n6
& sum(n6,n1) = n7
& sum(n6,n2) = n8
& sum(n6,n3) = n9
& sum(n6,n4) = n10
& sum(n6,n5) = n11
& sum(n6,n6) = n12
& sum(n6,n7) = n13
& sum(n6,n8) = n14
& sum(n6,n9) = n15
& sum(n6,n10) = n0
& sum(n6,n11) = n1
& sum(n6,n12) = n2
& sum(n6,n13) = n3
& sum(n6,n14) = n4
& sum(n6,n15) = n5
& sum(n7,n0) = n7
& sum(n7,n1) = n8
& sum(n7,n2) = n9
& sum(n7,n3) = n10
& sum(n7,n4) = n11
& sum(n7,n5) = n12
& sum(n7,n6) = n13
& sum(n7,n7) = n14
& sum(n7,n8) = n15
& sum(n7,n9) = n0
& sum(n7,n10) = n1
& sum(n7,n11) = n2
& sum(n7,n12) = n3
& sum(n7,n13) = n4
& sum(n7,n14) = n5
& sum(n7,n15) = n6
& sum(n8,n0) = n8
& sum(n8,n1) = n9
& sum(n8,n2) = n10
& sum(n8,n3) = n11
& sum(n8,n4) = n12
& sum(n8,n5) = n13
& sum(n8,n6) = n14
& sum(n8,n7) = n15
& sum(n8,n8) = n0
& sum(n8,n9) = n1
& sum(n8,n10) = n2
& sum(n8,n11) = n3
& sum(n8,n12) = n4
& sum(n8,n13) = n5
& sum(n8,n14) = n6
& sum(n8,n15) = n7
& sum(n9,n0) = n9
& sum(n9,n1) = n10
& sum(n9,n2) = n11
& sum(n9,n3) = n12
& sum(n9,n4) = n13
& sum(n9,n5) = n14
& sum(n9,n6) = n15
& sum(n9,n7) = n0
& sum(n9,n8) = n1
& sum(n9,n9) = n2
& sum(n9,n10) = n3
& sum(n9,n11) = n4
& sum(n9,n12) = n5
& sum(n9,n13) = n6
& sum(n9,n14) = n7
& sum(n9,n15) = n8
& sum(n10,n0) = n10
& sum(n10,n1) = n11
& sum(n10,n2) = n12
& sum(n10,n3) = n13
& sum(n10,n4) = n14
& sum(n10,n5) = n15
& sum(n10,n6) = n0
& sum(n10,n7) = n1
& sum(n10,n8) = n2
& sum(n10,n9) = n3
& sum(n10,n10) = n4
& sum(n10,n11) = n5
& sum(n10,n12) = n6
& sum(n10,n13) = n7
& sum(n10,n14) = n8
& sum(n10,n15) = n9
& sum(n11,n0) = n11
& sum(n11,n1) = n12
& sum(n11,n2) = n13
& sum(n11,n3) = n14
& sum(n11,n4) = n15
& sum(n11,n5) = n0
& sum(n11,n6) = n1
& sum(n11,n7) = n2
& sum(n11,n8) = n3
& sum(n11,n9) = n4
& sum(n11,n10) = n5
& sum(n11,n11) = n6
& sum(n11,n12) = n7
& sum(n11,n13) = n8
& sum(n11,n14) = n9
& sum(n11,n15) = n10
& sum(n12,n0) = n12
& sum(n12,n1) = n13
& sum(n12,n2) = n14
& sum(n12,n3) = n15
& sum(n12,n4) = n0
& sum(n12,n5) = n1
& sum(n12,n6) = n2
& sum(n12,n7) = n3
& sum(n12,n8) = n4
& sum(n12,n9) = n5
& sum(n12,n10) = n6
& sum(n12,n11) = n7
& sum(n12,n12) = n8
& sum(n12,n13) = n9
& sum(n12,n14) = n10
& sum(n12,n15) = n11
& sum(n13,n0) = n13
& sum(n13,n1) = n14
& sum(n13,n2) = n15
& sum(n13,n3) = n0
& sum(n13,n4) = n1
& sum(n13,n5) = n2
& sum(n13,n6) = n3
& sum(n13,n7) = n4
& sum(n13,n8) = n5
& sum(n13,n9) = n6
& sum(n13,n10) = n7
& sum(n13,n11) = n8
& sum(n13,n12) = n9
& sum(n13,n13) = n10
& sum(n13,n14) = n11
& sum(n13,n15) = n12
& sum(n14,n0) = n14
& sum(n14,n1) = n15
& sum(n14,n2) = n0
& sum(n14,n3) = n1
& sum(n14,n4) = n2
& sum(n14,n5) = n3
& sum(n14,n6) = n4
& sum(n14,n7) = n5
& sum(n14,n8) = n6
& sum(n14,n9) = n7
& sum(n14,n10) = n8
& sum(n14,n11) = n9
& sum(n14,n12) = n10
& sum(n14,n13) = n11
& sum(n14,n14) = n12
& sum(n14,n15) = n13
& sum(n15,n0) = n15
& sum(n15,n1) = n0
& sum(n15,n2) = n1
& sum(n15,n3) = n2
& sum(n15,n4) = n3
& sum(n15,n5) = n4
& sum(n15,n6) = n5
& sum(n15,n7) = n6
& sum(n15,n8) = n7
& sum(n15,n9) = n8
& sum(n15,n10) = n9
& sum(n15,n11) = n10
& sum(n15,n12) = n11
& sum(n15,n13) = n12
& sum(n15,n14) = n13
& sum(n15,n15) = n14
& ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6
| X0 = n7
| X0 = n8
| X0 = n9
| X0 = n10
| X0 = n11
| X0 = n12
| X0 = n13
| X0 = n14
| X0 = n15 )
& ( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| X1 = n4
| X1 = n5
| X1 = n6
| X1 = n7
| X1 = n8
| X1 = n9
| X1 = n10
| X1 = n11
| X1 = n12
| X1 = n13
| X1 = n14
| X1 = n15 )
& X42 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X0))))))))))))))))
& X44 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X0))))))))))))))))
& X43 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X1))))))))))))))))
& X45 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X1))))))))))))))))
& X46 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X2))))))))))))))))
& X48 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X2))))))))))))))))
& X47 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X3))))))))))))))))
& X49 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X3))))))))))))))))
& X50 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X4))))))))))))))))
& X52 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X4))))))))))))))))
& X51 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X5))))))))))))))))
& X53 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X5))))))))))))))))
& X54 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X6))))))))))))))))
& X56 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X6))))))))))))))))
& X55 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X7))))))))))))))))
& X57 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X7))))))))))))))))
& X58 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X8))))))))))))))))
& X60 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X8))))))))))))))))
& X59 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X9))))))))))))))))
& X61 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X9))))))))))))))))
& X62 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X10))))))))))))))))
& X64 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X10))))))))))))))))
& X63 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X11))))))))))))))))
& X65 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X11))))))))))))))))
& X66 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X12))))))))))))))))
& X68 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X12))))))))))))))))
& X67 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X13))))))))))))))))
& X69 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X13))))))))))))))))
& X70 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X14))))))))))))))))
& X72 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X14))))))))))))))))
& X71 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X15))))))))))))))))
& X73 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X15))))))))))))))))
& X74 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X16))))))))))))))))
& X76 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X16))))))))))))))))
& X75 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X17))))))))))))))))
& X77 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X17))))))))))))))))
& X78 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X18))))))))))))))))
& X80 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X18))))))))))))))))
& X79 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X19))))))))))))))))
& X81 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X19))))))))))))))))
& X82 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X20))))))))))))))))
& X84 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X20))))))))))))))))
& X83 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X21))))))))))))))))
& X85 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X21))))))))))))))))
& X86 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X22))))))))))))))))
& X88 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X22))))))))))))))))
& X87 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X23))))))))))))))))
& X89 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X23))))))))))))))))
& X90 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X24))))))))))))))))
& X92 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X24))))))))))))))))
& X91 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X25))))))))))))))))
& X93 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X25))))))))))))))))
& X94 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X26))))))))))))))))
& X96 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X26))))))))))))))))
& X95 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X27))))))))))))))))
& X97 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X27))))))))))))))))
& X98 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X28))))))))))))))))
& X100 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X28))))))))))))))))
& X99 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X29))))))))))))))))
& X101 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X29))))))))))))))))
& X102 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X30))))))))))))))))
& X104 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X30))))))))))))))))
& X103 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X31))))))))))))))))
& X105 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X31))))))))))))))))
& X106 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X32))))))))))))))))
& X108 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X32))))))))))))))))
& X107 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X33))))))))))))))))
& X109 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X33))))))))))))))))
& X110 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X34))))))))))))))))
& X112 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X34))))))))))))))))
& X111 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X35))))))))))))))))
& X113 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X35))))))))))))))))
& X114 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X36))))))))))))))))
& X116 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X36))))))))))))))))
& X115 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X37))))))))))))))))
& X117 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X37))))))))))))))))
& X118 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X38))))))))))))))))
& X120 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X38))))))))))))))))
& X119 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X39))))))))))))))))
& X121 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X39))))))))))))))))
& X2 = sum(sum(pred(X0),succ(X1)),sum(pred(X1),succ(X0)))
& X3 = sum(pred(X44),sum(succ(X42),sum(pred(X45),succ(X43))))
& X4 = sum(sum(pred(X2),succ(X3)),sum(pred(X3),succ(X2)))
& X5 = sum(pred(X48),sum(succ(X46),sum(pred(X49),succ(X47))))
& X6 = sum(sum(pred(X4),succ(X5)),sum(pred(X5),succ(X4)))
& X7 = sum(pred(X52),sum(succ(X50),sum(pred(X53),succ(X51))))
& X8 = sum(sum(pred(X6),succ(X7)),sum(pred(X7),succ(X6)))
& X9 = sum(pred(X56),sum(succ(X54),sum(pred(X57),succ(X55))))
& X10 = sum(sum(pred(X8),succ(X9)),sum(pred(X9),succ(X8)))
& X11 = sum(pred(X60),sum(succ(X58),sum(pred(X61),succ(X59))))
& X12 = sum(sum(pred(X10),succ(X11)),sum(pred(X11),succ(X10)))
& X13 = sum(pred(X64),sum(succ(X62),sum(pred(X65),succ(X63))))
& X14 = sum(sum(pred(X12),succ(X13)),sum(pred(X13),succ(X12)))
& X15 = sum(pred(X68),sum(succ(X66),sum(pred(X69),succ(X67))))
& X16 = sum(sum(pred(X14),succ(X15)),sum(pred(X15),succ(X14)))
& X17 = sum(pred(X72),sum(succ(X70),sum(pred(X73),succ(X71))))
& X18 = sum(sum(pred(X16),succ(X17)),sum(pred(X17),succ(X16)))
& X19 = sum(pred(X76),sum(succ(X74),sum(pred(X77),succ(X75))))
& X20 = sum(sum(pred(X18),succ(X19)),sum(pred(X19),succ(X18)))
& X21 = sum(pred(X80),sum(succ(X78),sum(pred(X81),succ(X79))))
& X22 = sum(sum(pred(X20),succ(X21)),sum(pred(X21),succ(X20)))
& X23 = sum(pred(X84),sum(succ(X82),sum(pred(X85),succ(X83))))
& X24 = sum(sum(pred(X22),succ(X23)),sum(pred(X23),succ(X22)))
& X25 = sum(pred(X88),sum(succ(X86),sum(pred(X89),succ(X87))))
& X26 = sum(sum(pred(X24),succ(X25)),sum(pred(X25),succ(X24)))
& X27 = sum(pred(X92),sum(succ(X90),sum(pred(X93),succ(X91))))
& X28 = sum(sum(pred(X26),succ(X27)),sum(pred(X27),succ(X26)))
& X29 = sum(pred(X96),sum(succ(X94),sum(pred(X97),succ(X95))))
& X30 = sum(sum(pred(X28),succ(X29)),sum(pred(X29),succ(X28)))
& X31 = sum(pred(X100),sum(succ(X98),sum(pred(X101),succ(X99))))
& X32 = sum(sum(pred(X30),succ(X31)),sum(pred(X31),succ(X30)))
& X33 = sum(pred(X104),sum(succ(X102),sum(pred(X105),succ(X103))))
& X34 = sum(sum(pred(X32),succ(X33)),sum(pred(X33),succ(X32)))
& X35 = sum(pred(X108),sum(succ(X106),sum(pred(X109),succ(X107))))
& X36 = sum(sum(pred(X34),succ(X35)),sum(pred(X35),succ(X34)))
& X37 = sum(pred(X112),sum(succ(X110),sum(pred(X113),succ(X111))))
& X38 = sum(sum(pred(X36),succ(X37)),sum(pred(X37),succ(X36)))
& X39 = sum(pred(X116),sum(succ(X114),sum(pred(X117),succ(X115))))
& X40 = sum(sum(pred(X38),succ(X39)),sum(pred(X39),succ(X38)))
& X41 = sum(pred(X120),sum(succ(X118),sum(pred(X121),succ(X119))))
& ( X34 != X35
| X36 != X37
| X38 != X39
| X40 != X41 )
& n0 != n1
& n0 != n2
& n0 != n3
& n0 != n4
& n0 != n5
& n0 != n6
& n0 != n7
& n0 != n8
& n0 != n9
& n0 != n10
& n0 != n11
& n0 != n12
& n0 != n13
& n0 != n14
& n0 != n15
& n1 != n2
& n1 != n3
& n1 != n4
& n1 != n5
& n1 != n6
& n1 != n7
& n1 != n8
& n1 != n9
& n1 != n10
& n1 != n11
& n1 != n12
& n1 != n13
& n1 != n14
& n1 != n15
& n2 != n3
& n2 != n4
& n2 != n5
& n2 != n6
& n2 != n7
& n2 != n8
& n2 != n9
& n2 != n10
& n2 != n11
& n2 != n12
& n2 != n13
& n2 != n14
& n2 != n15
& n3 != n4
& n3 != n5
& n3 != n6
& n3 != n7
& n3 != n8
& n3 != n9
& n3 != n10
& n3 != n11
& n3 != n12
& n3 != n13
& n3 != n14
& n3 != n15
& n4 != n5
& n4 != n6
& n4 != n7
& n4 != n8
& n4 != n9
& n4 != n10
& n4 != n11
& n4 != n12
& n4 != n13
& n4 != n14
& n4 != n15
& n5 != n6
& n5 != n7
& n5 != n8
& n5 != n9
& n5 != n10
& n5 != n11
& n5 != n12
& n5 != n13
& n5 != n14
& n5 != n15
& n6 != n7
& n6 != n8
& n6 != n9
& n6 != n10
& n6 != n11
& n6 != n12
& n6 != n13
& n6 != n14
& n6 != n15
& n7 != n8
& n7 != n9
& n7 != n10
& n7 != n11
& n7 != n12
& n7 != n13
& n7 != n14
& n7 != n15
& n8 != n9
& n8 != n10
& n8 != n11
& n8 != n12
& n8 != n13
& n8 != n14
& n8 != n15
& n9 != n10
& n9 != n11
& n9 != n12
& n9 != n13
& n9 != n14
& n9 != n15
& n10 != n11
& n10 != n12
& n10 != n13
& n10 != n14
& n10 != n15
& n11 != n12
& n11 != n13
& n11 != n14
& n11 != n15
& n12 != n13
& n12 != n14
& n12 != n15
& n13 != n14
& n13 != n15
& n14 != n15 ),
file('/export/starexec/sandbox/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) = n11
& succ(n11) = n12
& succ(n12) = n13
& succ(n13) = n14
& succ(n14) = n15
& succ(n15) = n0
& pred(n0) = n15
& 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
& pred(n11) = n10
& pred(n12) = n11
& pred(n13) = n12
& pred(n14) = n13
& pred(n15) = n14
& 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(n0,n11) = n11
& sum(n0,n12) = n12
& sum(n0,n13) = n13
& sum(n0,n14) = n14
& sum(n0,n15) = n15
& 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) = n11
& sum(n1,n11) = n12
& sum(n1,n12) = n13
& sum(n1,n13) = n14
& sum(n1,n14) = n15
& sum(n1,n15) = 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) = n11
& sum(n2,n10) = n12
& sum(n2,n11) = n13
& sum(n2,n12) = n14
& sum(n2,n13) = n15
& sum(n2,n14) = n0
& sum(n2,n15) = 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) = n11
& sum(n3,n9) = n12
& sum(n3,n10) = n13
& sum(n3,n11) = n14
& sum(n3,n12) = n15
& sum(n3,n13) = n0
& sum(n3,n14) = n1
& sum(n3,n15) = 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) = n11
& sum(n4,n8) = n12
& sum(n4,n9) = n13
& sum(n4,n10) = n14
& sum(n4,n11) = n15
& sum(n4,n12) = n0
& sum(n4,n13) = n1
& sum(n4,n14) = n2
& sum(n4,n15) = 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) = n11
& sum(n5,n7) = n12
& sum(n5,n8) = n13
& sum(n5,n9) = n14
& sum(n5,n10) = n15
& sum(n5,n11) = n0
& sum(n5,n12) = n1
& sum(n5,n13) = n2
& sum(n5,n14) = n3
& sum(n5,n15) = n4
& sum(n6,n0) = n6
& sum(n6,n1) = n7
& sum(n6,n2) = n8
& sum(n6,n3) = n9
& sum(n6,n4) = n10
& sum(n6,n5) = n11
& sum(n6,n6) = n12
& sum(n6,n7) = n13
& sum(n6,n8) = n14
& sum(n6,n9) = n15
& sum(n6,n10) = n0
& sum(n6,n11) = n1
& sum(n6,n12) = n2
& sum(n6,n13) = n3
& sum(n6,n14) = n4
& sum(n6,n15) = n5
& sum(n7,n0) = n7
& sum(n7,n1) = n8
& sum(n7,n2) = n9
& sum(n7,n3) = n10
& sum(n7,n4) = n11
& sum(n7,n5) = n12
& sum(n7,n6) = n13
& sum(n7,n7) = n14
& sum(n7,n8) = n15
& sum(n7,n9) = n0
& sum(n7,n10) = n1
& sum(n7,n11) = n2
& sum(n7,n12) = n3
& sum(n7,n13) = n4
& sum(n7,n14) = n5
& sum(n7,n15) = n6
& sum(n8,n0) = n8
& sum(n8,n1) = n9
& sum(n8,n2) = n10
& sum(n8,n3) = n11
& sum(n8,n4) = n12
& sum(n8,n5) = n13
& sum(n8,n6) = n14
& sum(n8,n7) = n15
& sum(n8,n8) = n0
& sum(n8,n9) = n1
& sum(n8,n10) = n2
& sum(n8,n11) = n3
& sum(n8,n12) = n4
& sum(n8,n13) = n5
& sum(n8,n14) = n6
& sum(n8,n15) = n7
& sum(n9,n0) = n9
& sum(n9,n1) = n10
& sum(n9,n2) = n11
& sum(n9,n3) = n12
& sum(n9,n4) = n13
& sum(n9,n5) = n14
& sum(n9,n6) = n15
& sum(n9,n7) = n0
& sum(n9,n8) = n1
& sum(n9,n9) = n2
& sum(n9,n10) = n3
& sum(n9,n11) = n4
& sum(n9,n12) = n5
& sum(n9,n13) = n6
& sum(n9,n14) = n7
& sum(n9,n15) = n8
& sum(n10,n0) = n10
& sum(n10,n1) = n11
& sum(n10,n2) = n12
& sum(n10,n3) = n13
& sum(n10,n4) = n14
& sum(n10,n5) = n15
& sum(n10,n6) = n0
& sum(n10,n7) = n1
& sum(n10,n8) = n2
& sum(n10,n9) = n3
& sum(n10,n10) = n4
& sum(n10,n11) = n5
& sum(n10,n12) = n6
& sum(n10,n13) = n7
& sum(n10,n14) = n8
& sum(n10,n15) = n9
& sum(n11,n0) = n11
& sum(n11,n1) = n12
& sum(n11,n2) = n13
& sum(n11,n3) = n14
& sum(n11,n4) = n15
& sum(n11,n5) = n0
& sum(n11,n6) = n1
& sum(n11,n7) = n2
& sum(n11,n8) = n3
& sum(n11,n9) = n4
& sum(n11,n10) = n5
& sum(n11,n11) = n6
& sum(n11,n12) = n7
& sum(n11,n13) = n8
& sum(n11,n14) = n9
& sum(n11,n15) = n10
& sum(n12,n0) = n12
& sum(n12,n1) = n13
& sum(n12,n2) = n14
& sum(n12,n3) = n15
& sum(n12,n4) = n0
& sum(n12,n5) = n1
& sum(n12,n6) = n2
& sum(n12,n7) = n3
& sum(n12,n8) = n4
& sum(n12,n9) = n5
& sum(n12,n10) = n6
& sum(n12,n11) = n7
& sum(n12,n12) = n8
& sum(n12,n13) = n9
& sum(n12,n14) = n10
& sum(n12,n15) = n11
& sum(n13,n0) = n13
& sum(n13,n1) = n14
& sum(n13,n2) = n15
& sum(n13,n3) = n0
& sum(n13,n4) = n1
& sum(n13,n5) = n2
& sum(n13,n6) = n3
& sum(n13,n7) = n4
& sum(n13,n8) = n5
& sum(n13,n9) = n6
& sum(n13,n10) = n7
& sum(n13,n11) = n8
& sum(n13,n12) = n9
& sum(n13,n13) = n10
& sum(n13,n14) = n11
& sum(n13,n15) = n12
& sum(n14,n0) = n14
& sum(n14,n1) = n15
& sum(n14,n2) = n0
& sum(n14,n3) = n1
& sum(n14,n4) = n2
& sum(n14,n5) = n3
& sum(n14,n6) = n4
& sum(n14,n7) = n5
& sum(n14,n8) = n6
& sum(n14,n9) = n7
& sum(n14,n10) = n8
& sum(n14,n11) = n9
& sum(n14,n12) = n10
& sum(n14,n13) = n11
& sum(n14,n14) = n12
& sum(n14,n15) = n13
& sum(n15,n0) = n15
& sum(n15,n1) = n0
& sum(n15,n2) = n1
& sum(n15,n3) = n2
& sum(n15,n4) = n3
& sum(n15,n5) = n4
& sum(n15,n6) = n5
& sum(n15,n7) = n6
& sum(n15,n8) = n7
& sum(n15,n9) = n8
& sum(n15,n10) = n9
& sum(n15,n11) = n10
& sum(n15,n12) = n11
& sum(n15,n13) = n12
& sum(n15,n14) = n13
& sum(n15,n15) = n14
& ( n0 = sK0
| n1 = sK0
| n2 = sK0
| n3 = sK0
| n4 = sK0
| n5 = sK0
| n6 = sK0
| n7 = sK0
| n8 = sK0
| n9 = sK0
| n10 = sK0
| n11 = sK0
| n12 = sK0
| n13 = sK0
| n14 = sK0
| n15 = sK0 )
& ( n0 = sK1
| n1 = sK1
| n2 = sK1
| n3 = sK1
| n4 = sK1
| n5 = sK1
| n6 = sK1
| n7 = sK1
| n8 = sK1
| n9 = sK1
| n10 = sK1
| n11 = sK1
| n12 = sK1
| n13 = sK1
| n14 = sK1
| n15 = sK1 )
& sK42 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK0))))))))))))))))
& sK44 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK0))))))))))))))))
& sK43 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK1))))))))))))))))
& sK45 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK1))))))))))))))))
& sK46 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK2))))))))))))))))
& sK48 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK2))))))))))))))))
& sK47 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK3))))))))))))))))
& sK49 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK3))))))))))))))))
& sK50 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK4))))))))))))))))
& sK52 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK4))))))))))))))))
& sK51 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK5))))))))))))))))
& sK53 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK5))))))))))))))))
& sK54 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK6))))))))))))))))
& sK56 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK6))))))))))))))))
& sK55 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK7))))))))))))))))
& sK57 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK7))))))))))))))))
& sK58 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK8))))))))))))))))
& sK60 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK8))))))))))))))))
& sK59 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK9))))))))))))))))
& sK61 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK9))))))))))))))))
& sK62 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK10))))))))))))))))
& sK64 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK10))))))))))))))))
& sK63 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK11))))))))))))))))
& sK65 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK11))))))))))))))))
& sK66 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK12))))))))))))))))
& sK68 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK12))))))))))))))))
& sK67 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK13))))))))))))))))
& sK69 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK13))))))))))))))))
& sK70 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK14))))))))))))))))
& sK72 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK14))))))))))))))))
& sK71 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK15))))))))))))))))
& sK73 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK15))))))))))))))))
& sK74 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK16))))))))))))))))
& sK76 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK16))))))))))))))))
& sK75 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK17))))))))))))))))
& sK77 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK17))))))))))))))))
& sK78 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK18))))))))))))))))
& sK80 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK18))))))))))))))))
& sK79 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK19))))))))))))))))
& sK81 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK19))))))))))))))))
& sK82 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK20))))))))))))))))
& sK84 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK20))))))))))))))))
& sK83 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK21))))))))))))))))
& sK85 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK21))))))))))))))))
& sK86 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK22))))))))))))))))
& sK88 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK22))))))))))))))))
& sK87 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK23))))))))))))))))
& sK89 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK23))))))))))))))))
& sK90 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK24))))))))))))))))
& sK92 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK24))))))))))))))))
& sK91 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK25))))))))))))))))
& sK93 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK25))))))))))))))))
& sK94 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK26))))))))))))))))
& sK96 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK26))))))))))))))))
& sK95 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK27))))))))))))))))
& sK97 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK27))))))))))))))))
& sK98 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK28))))))))))))))))
& sK100 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK28))))))))))))))))
& sK99 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK29))))))))))))))))
& sK101 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK29))))))))))))))))
& sK102 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK30))))))))))))))))
& sK104 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK30))))))))))))))))
& sK103 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK31))))))))))))))))
& sK105 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK31))))))))))))))))
& sK106 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK32))))))))))))))))
& sK108 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK32))))))))))))))))
& sK107 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK33))))))))))))))))
& sK109 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK33))))))))))))))))
& sK110 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK34))))))))))))))))
& sK112 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK34))))))))))))))))
& sK111 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK35))))))))))))))))
& sK113 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK35))))))))))))))))
& sK114 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK36))))))))))))))))
& sK116 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK36))))))))))))))))
& sK115 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK37))))))))))))))))
& sK117 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK37))))))))))))))))
& sK118 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK38))))))))))))))))
& sK120 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK38))))))))))))))))
& sK119 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK39))))))))))))))))
& sK121 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK39))))))))))))))))
& sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
& sK3 = sum(pred(sK44),sum(succ(sK42),sum(pred(sK45),succ(sK43))))
& sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
& sK5 = sum(pred(sK48),sum(succ(sK46),sum(pred(sK49),succ(sK47))))
& sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
& sK7 = sum(pred(sK52),sum(succ(sK50),sum(pred(sK53),succ(sK51))))
& sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
& sK9 = sum(pred(sK56),sum(succ(sK54),sum(pred(sK57),succ(sK55))))
& sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
& sK11 = sum(pred(sK60),sum(succ(sK58),sum(pred(sK61),succ(sK59))))
& sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10)))
& sK13 = sum(pred(sK64),sum(succ(sK62),sum(pred(sK65),succ(sK63))))
& sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12)))
& sK15 = sum(pred(sK68),sum(succ(sK66),sum(pred(sK69),succ(sK67))))
& sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14)))
& sK17 = sum(pred(sK72),sum(succ(sK70),sum(pred(sK73),succ(sK71))))
& sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16)))
& sK19 = sum(pred(sK76),sum(succ(sK74),sum(pred(sK77),succ(sK75))))
& sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18)))
& sK21 = sum(pred(sK80),sum(succ(sK78),sum(pred(sK81),succ(sK79))))
& sK22 = sum(sum(pred(sK20),succ(sK21)),sum(pred(sK21),succ(sK20)))
& sK23 = sum(pred(sK84),sum(succ(sK82),sum(pred(sK85),succ(sK83))))
& sK24 = sum(sum(pred(sK22),succ(sK23)),sum(pred(sK23),succ(sK22)))
& sK25 = sum(pred(sK88),sum(succ(sK86),sum(pred(sK89),succ(sK87))))
& sK26 = sum(sum(pred(sK24),succ(sK25)),sum(pred(sK25),succ(sK24)))
& sK27 = sum(pred(sK92),sum(succ(sK90),sum(pred(sK93),succ(sK91))))
& sK28 = sum(sum(pred(sK26),succ(sK27)),sum(pred(sK27),succ(sK26)))
& sK29 = sum(pred(sK96),sum(succ(sK94),sum(pred(sK97),succ(sK95))))
& sK30 = sum(sum(pred(sK28),succ(sK29)),sum(pred(sK29),succ(sK28)))
& sK31 = sum(pred(sK100),sum(succ(sK98),sum(pred(sK101),succ(sK99))))
& sK32 = sum(sum(pred(sK30),succ(sK31)),sum(pred(sK31),succ(sK30)))
& sK33 = sum(pred(sK104),sum(succ(sK102),sum(pred(sK105),succ(sK103))))
& sK34 = sum(sum(pred(sK32),succ(sK33)),sum(pred(sK33),succ(sK32)))
& sK35 = sum(pred(sK108),sum(succ(sK106),sum(pred(sK109),succ(sK107))))
& sK36 = sum(sum(pred(sK34),succ(sK35)),sum(pred(sK35),succ(sK34)))
& sK37 = sum(pred(sK112),sum(succ(sK110),sum(pred(sK113),succ(sK111))))
& sK38 = sum(sum(pred(sK36),succ(sK37)),sum(pred(sK37),succ(sK36)))
& sK39 = sum(pred(sK116),sum(succ(sK114),sum(pred(sK117),succ(sK115))))
& sK40 = sum(sum(pred(sK38),succ(sK39)),sum(pred(sK39),succ(sK38)))
& sK41 = sum(pred(sK120),sum(succ(sK118),sum(pred(sK121),succ(sK119))))
& ( sK34 != sK35
| sK36 != sK37
| sK38 != sK39
| sK40 != sK41 )
& n0 != n1
& n0 != n2
& n0 != n3
& n0 != n4
& n0 != n5
& n0 != n6
& n0 != n7
& n0 != n8
& n0 != n9
& n0 != n10
& n0 != n11
& n0 != n12
& n0 != n13
& n0 != n14
& n0 != n15
& n1 != n2
& n1 != n3
& n1 != n4
& n1 != n5
& n1 != n6
& n1 != n7
& n1 != n8
& n1 != n9
& n1 != n10
& n1 != n11
& n1 != n12
& n1 != n13
& n1 != n14
& n1 != n15
& n2 != n3
& n2 != n4
& n2 != n5
& n2 != n6
& n2 != n7
& n2 != n8
& n2 != n9
& n2 != n10
& n2 != n11
& n2 != n12
& n2 != n13
& n2 != n14
& n2 != n15
& n3 != n4
& n3 != n5
& n3 != n6
& n3 != n7
& n3 != n8
& n3 != n9
& n3 != n10
& n3 != n11
& n3 != n12
& n3 != n13
& n3 != n14
& n3 != n15
& n4 != n5
& n4 != n6
& n4 != n7
& n4 != n8
& n4 != n9
& n4 != n10
& n4 != n11
& n4 != n12
& n4 != n13
& n4 != n14
& n4 != n15
& n5 != n6
& n5 != n7
& n5 != n8
& n5 != n9
& n5 != n10
& n5 != n11
& n5 != n12
& n5 != n13
& n5 != n14
& n5 != n15
& n6 != n7
& n6 != n8
& n6 != n9
& n6 != n10
& n6 != n11
& n6 != n12
& n6 != n13
& n6 != n14
& n6 != n15
& n7 != n8
& n7 != n9
& n7 != n10
& n7 != n11
& n7 != n12
& n7 != n13
& n7 != n14
& n7 != n15
& n8 != n9
& n8 != n10
& n8 != n11
& n8 != n12
& n8 != n13
& n8 != n14
& n8 != n15
& n9 != n10
& n9 != n11
& n9 != n12
& n9 != n13
& n9 != n14
& n9 != n15
& n10 != n11
& n10 != n12
& n10 != n13
& n10 != n14
& n10 != n15
& n11 != n12
& n11 != n13
& n11 != n14
& n11 != n15
& n12 != n13
& n12 != n14
& n12 != n15
& n13 != n14
& n13 != n15
& n14 != n15 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49,sK50,sK51,sK52,sK53,sK54,sK55,sK56,sK57,sK58,sK59,sK60,sK61,sK62,sK63,sK64,sK65,sK66,sK67,sK68,sK69,sK70,sK71,sK72,sK73,sK74,sK75,sK76,sK77,sK78,sK79,sK80,sK81,sK82,sK83,sK84,sK85,sK86,sK87,sK88,sK89,sK90,sK91,sK92,sK93,sK94,sK95,sK96,sK97,sK98,sK99,sK100,sK101,sK102,sK103,sK104,sK105,sK106,sK107,sK108,sK109,sK110,sK111,sK112,sK113,sK114,sK115,sK116,sK117,sK118,sK119,sK120,sK121]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X8,sK8),skolemize(X9,sK9),skolemize(X10,sK10),skolemize(X11,sK11),skolemize(X12,sK12),skolemize(X13,sK13),skolemize(X14,sK14),skolemize(X15,sK15),skolemize(X16,sK16),skolemize(X17,sK17),skolemize(X18,sK18),skolemize(X19,sK19),skolemize(X20,sK20),skolemize(X21,sK21),skolemize(X22,sK22),skolemize(X23,sK23),skolemize(X24,sK24),skolemize(X25,sK25),skolemize(X26,sK26),skolemize(X27,sK27),skolemize(X28,sK28),skolemize(X29,sK29),skolemize(X30,sK30),skolemize(X31,sK31),skolemize(X32,sK32),skolemize(X33,sK33),skolemize(X34,sK34),skolemize(X35,sK35),skolemize(X36,sK36),skolemize(X37,sK37),skolemize(X38,sK38),skolemize(X39,sK39),skolemize(X40,sK40),skolemize(X41,sK41),skolemize(X42,sK42),skolemize(X43,sK43),skolemize(X44,sK44),skolemize(X45,sK45),skolemize(X46,sK46),skolemize(X47,sK47),skolemize(X48,sK48),skolemize(X49,sK49),skolemize(X50,sK50),skolemize(X51,sK51),skolemize(X52,sK52),skolemize(X53,sK53),skolemize(X54,sK54),skolemize(X55,sK55),skolemize(X56,sK56),skolemize(X57,sK57),skolemize(X58,sK58),skolemize(X59,sK59),skolemize(X60,sK60),skolemize(X61,sK61),skolemize(X62,sK62),skolemize(X63,sK63),skolemize(X64,sK64),skolemize(X65,sK65),skolemize(X66,sK66),skolemize(X67,sK67),skolemize(X68,sK68),skolemize(X69,sK69),skolemize(X70,sK70),skolemize(X71,sK71),skolemize(X72,sK72),skolemize(X73,sK73),skolemize(X74,sK74),skolemize(X75,sK75),skolemize(X76,sK76),skolemize(X77,sK77),skolemize(X78,sK78),skolemize(X79,sK79),skolemize(X80,sK80),skolemize(X81,sK81),skolemize(X82,sK82),skolemize(X83,sK83),skolemize(X84,sK84),skolemize(X85,sK85),skolemize(X86,sK86),skolemize(X87,sK87),skolemize(X88,sK88),skolemize(X89,sK89),skolemize(X90,sK90),skolemize(X91,sK91),skolemize(X92,sK92),skolemize(X93,sK93),skolemize(X94,sK94),skolemize(X95,sK95),skolemize(X96,sK96),skolemize(X97,sK97),skolemize(X98,sK98),skolemize(X99,sK99),skolemize(X100,sK100),skolemize(X101,sK101),skolemize(X102,sK102),skolemize(X103,sK103),skolemize(X104,sK104),skolemize(X105,sK105),skolemize(X106,sK106),skolemize(X107,sK107),skolemize(X108,sK108),skolemize(X109,sK109),skolemize(X110,sK110),skolemize(X111,sK111),skolemize(X112,sK112),skolemize(X113,sK113),skolemize(X114,sK114),skolemize(X115,sK115),skolemize(X116,sK116),skolemize(X117,sK117),skolemize(X118,sK118),skolemize(X119,sK119),skolemize(X120,sK120),skolemize(X121,sK121)],[f1]) ).
fof(f123,plain,
( sK34 != sK35
| sK36 != sK37
| sK38 != sK39
| sK40 != sK41 ),
inference(cnf_transformation,[],[f2]) ).
fof(f124,plain,
sK41 = sum(pred(sK120),sum(succ(sK118),sum(pred(sK121),succ(sK119)))),
inference(cnf_transformation,[],[f2]) ).
fof(f125,plain,
sK40 = sum(sum(pred(sK38),succ(sK39)),sum(pred(sK39),succ(sK38))),
inference(cnf_transformation,[],[f2]) ).
fof(f126,plain,
sK39 = sum(pred(sK116),sum(succ(sK114),sum(pred(sK117),succ(sK115)))),
inference(cnf_transformation,[],[f2]) ).
fof(f127,plain,
sK38 = sum(sum(pred(sK36),succ(sK37)),sum(pred(sK37),succ(sK36))),
inference(cnf_transformation,[],[f2]) ).
fof(f128,plain,
sK37 = sum(pred(sK112),sum(succ(sK110),sum(pred(sK113),succ(sK111)))),
inference(cnf_transformation,[],[f2]) ).
fof(f129,plain,
sK36 = sum(sum(pred(sK34),succ(sK35)),sum(pred(sK35),succ(sK34))),
inference(cnf_transformation,[],[f2]) ).
fof(f130,plain,
sK35 = sum(pred(sK108),sum(succ(sK106),sum(pred(sK109),succ(sK107)))),
inference(cnf_transformation,[],[f2]) ).
fof(f131,plain,
sK34 = sum(sum(pred(sK32),succ(sK33)),sum(pred(sK33),succ(sK32))),
inference(cnf_transformation,[],[f2]) ).
fof(f132,plain,
sK33 = sum(pred(sK104),sum(succ(sK102),sum(pred(sK105),succ(sK103)))),
inference(cnf_transformation,[],[f2]) ).
fof(f133,plain,
sK32 = sum(sum(pred(sK30),succ(sK31)),sum(pred(sK31),succ(sK30))),
inference(cnf_transformation,[],[f2]) ).
fof(f134,plain,
sK31 = sum(pred(sK100),sum(succ(sK98),sum(pred(sK101),succ(sK99)))),
inference(cnf_transformation,[],[f2]) ).
fof(f135,plain,
sK30 = sum(sum(pred(sK28),succ(sK29)),sum(pred(sK29),succ(sK28))),
inference(cnf_transformation,[],[f2]) ).
fof(f136,plain,
sK29 = sum(pred(sK96),sum(succ(sK94),sum(pred(sK97),succ(sK95)))),
inference(cnf_transformation,[],[f2]) ).
fof(f137,plain,
sK28 = sum(sum(pred(sK26),succ(sK27)),sum(pred(sK27),succ(sK26))),
inference(cnf_transformation,[],[f2]) ).
fof(f138,plain,
sK27 = sum(pred(sK92),sum(succ(sK90),sum(pred(sK93),succ(sK91)))),
inference(cnf_transformation,[],[f2]) ).
fof(f139,plain,
sK26 = sum(sum(pred(sK24),succ(sK25)),sum(pred(sK25),succ(sK24))),
inference(cnf_transformation,[],[f2]) ).
fof(f140,plain,
sK25 = sum(pred(sK88),sum(succ(sK86),sum(pred(sK89),succ(sK87)))),
inference(cnf_transformation,[],[f2]) ).
fof(f141,plain,
sK24 = sum(sum(pred(sK22),succ(sK23)),sum(pred(sK23),succ(sK22))),
inference(cnf_transformation,[],[f2]) ).
fof(f142,plain,
sK23 = sum(pred(sK84),sum(succ(sK82),sum(pred(sK85),succ(sK83)))),
inference(cnf_transformation,[],[f2]) ).
fof(f143,plain,
sK22 = sum(sum(pred(sK20),succ(sK21)),sum(pred(sK21),succ(sK20))),
inference(cnf_transformation,[],[f2]) ).
fof(f144,plain,
sK21 = sum(pred(sK80),sum(succ(sK78),sum(pred(sK81),succ(sK79)))),
inference(cnf_transformation,[],[f2]) ).
fof(f145,plain,
sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18))),
inference(cnf_transformation,[],[f2]) ).
fof(f146,plain,
sK19 = sum(pred(sK76),sum(succ(sK74),sum(pred(sK77),succ(sK75)))),
inference(cnf_transformation,[],[f2]) ).
fof(f147,plain,
sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16))),
inference(cnf_transformation,[],[f2]) ).
fof(f148,plain,
sK17 = sum(pred(sK72),sum(succ(sK70),sum(pred(sK73),succ(sK71)))),
inference(cnf_transformation,[],[f2]) ).
fof(f149,plain,
sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14))),
inference(cnf_transformation,[],[f2]) ).
fof(f150,plain,
sK15 = sum(pred(sK68),sum(succ(sK66),sum(pred(sK69),succ(sK67)))),
inference(cnf_transformation,[],[f2]) ).
fof(f151,plain,
sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12))),
inference(cnf_transformation,[],[f2]) ).
fof(f152,plain,
sK13 = sum(pred(sK64),sum(succ(sK62),sum(pred(sK65),succ(sK63)))),
inference(cnf_transformation,[],[f2]) ).
fof(f153,plain,
sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10))),
inference(cnf_transformation,[],[f2]) ).
fof(f154,plain,
sK11 = sum(pred(sK60),sum(succ(sK58),sum(pred(sK61),succ(sK59)))),
inference(cnf_transformation,[],[f2]) ).
fof(f155,plain,
sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8))),
inference(cnf_transformation,[],[f2]) ).
fof(f156,plain,
sK9 = sum(pred(sK56),sum(succ(sK54),sum(pred(sK57),succ(sK55)))),
inference(cnf_transformation,[],[f2]) ).
fof(f157,plain,
sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6))),
inference(cnf_transformation,[],[f2]) ).
fof(f158,plain,
sK7 = sum(pred(sK52),sum(succ(sK50),sum(pred(sK53),succ(sK51)))),
inference(cnf_transformation,[],[f2]) ).
fof(f159,plain,
sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4))),
inference(cnf_transformation,[],[f2]) ).
fof(f160,plain,
sK5 = sum(pred(sK48),sum(succ(sK46),sum(pred(sK49),succ(sK47)))),
inference(cnf_transformation,[],[f2]) ).
fof(f161,plain,
sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2))),
inference(cnf_transformation,[],[f2]) ).
fof(f162,plain,
sK3 = sum(pred(sK44),sum(succ(sK42),sum(pred(sK45),succ(sK43)))),
inference(cnf_transformation,[],[f2]) ).
fof(f163,plain,
sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0))),
inference(cnf_transformation,[],[f2]) ).
fof(f164,plain,
sK121 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK39)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f165,plain,
sK119 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK39)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f166,plain,
sK120 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK38)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f167,plain,
sK118 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK38)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f168,plain,
sK117 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK37)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f169,plain,
sK115 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK37)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f170,plain,
sK116 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK36)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f171,plain,
sK114 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK36)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f172,plain,
sK113 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK35)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f173,plain,
sK111 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK35)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f174,plain,
sK112 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK34)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f175,plain,
sK110 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK34)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f176,plain,
sK109 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK33)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f177,plain,
sK107 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK33)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f178,plain,
sK108 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK32)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f179,plain,
sK106 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK32)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f180,plain,
sK105 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK31)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f181,plain,
sK103 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK31)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f182,plain,
sK104 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK30)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f183,plain,
sK102 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK30)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f184,plain,
sK101 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK29)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f185,plain,
sK99 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK29)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f186,plain,
sK100 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK28)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f187,plain,
sK98 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK28)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f188,plain,
sK97 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK27)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f189,plain,
sK95 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK27)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f190,plain,
sK96 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK26)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f191,plain,
sK94 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK26)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f192,plain,
sK93 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK25)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f193,plain,
sK91 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK25)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f194,plain,
sK92 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK24)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f195,plain,
sK90 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK24)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f196,plain,
sK89 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK23)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f197,plain,
sK87 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK23)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f198,plain,
sK88 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK22)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f199,plain,
sK86 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK22)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f200,plain,
sK85 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK21)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f201,plain,
sK83 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK21)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f202,plain,
sK84 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK20)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f203,plain,
sK82 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK20)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f204,plain,
sK81 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK19)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f205,plain,
sK79 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK19)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f206,plain,
sK80 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK18)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f207,plain,
sK78 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK18)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f208,plain,
sK77 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK17)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f209,plain,
sK75 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK17)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f210,plain,
sK76 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK16)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f211,plain,
sK74 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK16)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f212,plain,
sK73 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK15)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f213,plain,
sK71 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK15)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f214,plain,
sK72 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK14)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f215,plain,
sK70 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK14)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f216,plain,
sK69 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK13)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f217,plain,
sK67 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK13)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f218,plain,
sK68 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK12)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f219,plain,
sK66 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK12)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f220,plain,
sK65 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK11)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f221,plain,
sK63 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK11)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f222,plain,
sK64 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK10)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f223,plain,
sK62 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK10)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f224,plain,
sK61 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK9)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f225,plain,
sK59 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK9)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f226,plain,
sK60 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK8)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f227,plain,
sK58 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK8)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f228,plain,
sK57 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK7)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f229,plain,
sK55 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK7)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f230,plain,
sK56 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK6)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f231,plain,
sK54 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK6)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f232,plain,
sK53 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK5)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f233,plain,
sK51 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK5)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f234,plain,
sK52 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK4)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f235,plain,
sK50 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK4)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f236,plain,
sK49 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK3)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f237,plain,
sK47 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK3)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f238,plain,
sK48 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK2)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f239,plain,
sK46 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK2)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f240,plain,
sK45 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK1)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f241,plain,
sK43 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK1)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f242,plain,
sK44 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK0)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f243,plain,
sK42 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK0)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f244,plain,
( n0 = sK1
| n1 = sK1
| n2 = sK1
| n3 = sK1
| n4 = sK1
| n5 = sK1
| n6 = sK1
| n7 = sK1
| n8 = sK1
| n9 = sK1
| n10 = sK1
| n11 = sK1
| n12 = sK1
| n13 = sK1
| n14 = sK1
| n15 = sK1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f245,plain,
( n0 = sK0
| n1 = sK0
| n2 = sK0
| n3 = sK0
| n4 = sK0
| n5 = sK0
| n6 = sK0
| n7 = sK0
| n8 = sK0
| n9 = sK0
| n10 = sK0
| n11 = sK0
| n12 = sK0
| n13 = sK0
| n14 = sK0
| n15 = sK0 ),
inference(cnf_transformation,[],[f2]) ).
fof(f246,plain,
n14 = sum(n15,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f247,plain,
n13 = sum(n15,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f248,plain,
n12 = sum(n15,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f249,plain,
n11 = sum(n15,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f250,plain,
n10 = sum(n15,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f251,plain,
n9 = sum(n15,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f252,plain,
n8 = sum(n15,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f253,plain,
n7 = sum(n15,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f254,plain,
n6 = sum(n15,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f255,plain,
n5 = sum(n15,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f256,plain,
n4 = sum(n15,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f257,plain,
n3 = sum(n15,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f258,plain,
n2 = sum(n15,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f259,plain,
n1 = sum(n15,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f260,plain,
n0 = sum(n15,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f261,plain,
n15 = sum(n15,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f262,plain,
n13 = sum(n14,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f263,plain,
n12 = sum(n14,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f264,plain,
n11 = sum(n14,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f265,plain,
n10 = sum(n14,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f266,plain,
n9 = sum(n14,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f267,plain,
n8 = sum(n14,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f268,plain,
n7 = sum(n14,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f269,plain,
n6 = sum(n14,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f270,plain,
n5 = sum(n14,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f271,plain,
n4 = sum(n14,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f272,plain,
n3 = sum(n14,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f273,plain,
n2 = sum(n14,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f274,plain,
n1 = sum(n14,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f275,plain,
n0 = sum(n14,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f276,plain,
n15 = sum(n14,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f277,plain,
n14 = sum(n14,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f278,plain,
n12 = sum(n13,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f279,plain,
n11 = sum(n13,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f280,plain,
n10 = sum(n13,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f281,plain,
n9 = sum(n13,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f282,plain,
n8 = sum(n13,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f283,plain,
n7 = sum(n13,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f284,plain,
n6 = sum(n13,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f285,plain,
n5 = sum(n13,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f286,plain,
n4 = sum(n13,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f287,plain,
n3 = sum(n13,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f288,plain,
n2 = sum(n13,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f289,plain,
n1 = sum(n13,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f290,plain,
n0 = sum(n13,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f291,plain,
n15 = sum(n13,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f292,plain,
n14 = sum(n13,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f293,plain,
n13 = sum(n13,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f294,plain,
n11 = sum(n12,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f295,plain,
n10 = sum(n12,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f296,plain,
n9 = sum(n12,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f297,plain,
n8 = sum(n12,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f298,plain,
n7 = sum(n12,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f299,plain,
n6 = sum(n12,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f300,plain,
n5 = sum(n12,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f301,plain,
n4 = sum(n12,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f302,plain,
n3 = sum(n12,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f303,plain,
n2 = sum(n12,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f304,plain,
n1 = sum(n12,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f305,plain,
n0 = sum(n12,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f306,plain,
n15 = sum(n12,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f307,plain,
n14 = sum(n12,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f308,plain,
n13 = sum(n12,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f309,plain,
n12 = sum(n12,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f310,plain,
n10 = sum(n11,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f311,plain,
n9 = sum(n11,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f312,plain,
n8 = sum(n11,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f313,plain,
n7 = sum(n11,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f314,plain,
n6 = sum(n11,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f315,plain,
n5 = sum(n11,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f316,plain,
n4 = sum(n11,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f317,plain,
n3 = sum(n11,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f318,plain,
n2 = sum(n11,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f319,plain,
n1 = sum(n11,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f320,plain,
n0 = sum(n11,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f321,plain,
n15 = sum(n11,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f322,plain,
n14 = sum(n11,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f323,plain,
n13 = sum(n11,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f324,plain,
n12 = sum(n11,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f325,plain,
n11 = sum(n11,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f326,plain,
n9 = sum(n10,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f327,plain,
n8 = sum(n10,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f328,plain,
n7 = sum(n10,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f329,plain,
n6 = sum(n10,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f330,plain,
n5 = sum(n10,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f331,plain,
n4 = sum(n10,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f332,plain,
n3 = sum(n10,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f333,plain,
n2 = sum(n10,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f334,plain,
n1 = sum(n10,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f335,plain,
n0 = sum(n10,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f336,plain,
n15 = sum(n10,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f337,plain,
n14 = sum(n10,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f338,plain,
n13 = sum(n10,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f339,plain,
n12 = sum(n10,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f340,plain,
n11 = sum(n10,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f341,plain,
n10 = sum(n10,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f342,plain,
n8 = sum(n9,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f343,plain,
n7 = sum(n9,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f344,plain,
n6 = sum(n9,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f345,plain,
n5 = sum(n9,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f346,plain,
n4 = sum(n9,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f347,plain,
n3 = sum(n9,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f348,plain,
n2 = sum(n9,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f349,plain,
n1 = sum(n9,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f350,plain,
n0 = sum(n9,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f351,plain,
n15 = sum(n9,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f352,plain,
n14 = sum(n9,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f353,plain,
n13 = sum(n9,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f354,plain,
n12 = sum(n9,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f355,plain,
n11 = sum(n9,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f356,plain,
n10 = sum(n9,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f357,plain,
n9 = sum(n9,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f358,plain,
n7 = sum(n8,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f359,plain,
n6 = sum(n8,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f360,plain,
n5 = sum(n8,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f361,plain,
n4 = sum(n8,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f362,plain,
n3 = sum(n8,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f363,plain,
n2 = sum(n8,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f364,plain,
n1 = sum(n8,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f365,plain,
n0 = sum(n8,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f366,plain,
n15 = sum(n8,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f367,plain,
n14 = sum(n8,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f368,plain,
n13 = sum(n8,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f369,plain,
n12 = sum(n8,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f370,plain,
n11 = sum(n8,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f371,plain,
n10 = sum(n8,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f372,plain,
n9 = sum(n8,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f373,plain,
n8 = sum(n8,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f374,plain,
n6 = sum(n7,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f375,plain,
n5 = sum(n7,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f376,plain,
n4 = sum(n7,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f377,plain,
n3 = sum(n7,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f378,plain,
n2 = sum(n7,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f379,plain,
n1 = sum(n7,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f380,plain,
n0 = sum(n7,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f381,plain,
n15 = sum(n7,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f382,plain,
n14 = sum(n7,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f383,plain,
n13 = sum(n7,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f384,plain,
n12 = sum(n7,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f385,plain,
n11 = sum(n7,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f386,plain,
n10 = sum(n7,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f387,plain,
n9 = sum(n7,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f388,plain,
n8 = sum(n7,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f389,plain,
n7 = sum(n7,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f390,plain,
n5 = sum(n6,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f391,plain,
n4 = sum(n6,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f392,plain,
n3 = sum(n6,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f393,plain,
n2 = sum(n6,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f394,plain,
n1 = sum(n6,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f395,plain,
n0 = sum(n6,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f396,plain,
n15 = sum(n6,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f397,plain,
n14 = sum(n6,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f398,plain,
n13 = sum(n6,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f399,plain,
n12 = sum(n6,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f400,plain,
n11 = sum(n6,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f401,plain,
n10 = sum(n6,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f402,plain,
n9 = sum(n6,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f403,plain,
n8 = sum(n6,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f404,plain,
n7 = sum(n6,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f405,plain,
n6 = sum(n6,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f406,plain,
n4 = sum(n5,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f407,plain,
n3 = sum(n5,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f408,plain,
n2 = sum(n5,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f409,plain,
n1 = sum(n5,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f410,plain,
n0 = sum(n5,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f411,plain,
n15 = sum(n5,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f412,plain,
n14 = sum(n5,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f413,plain,
n13 = sum(n5,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f414,plain,
n12 = sum(n5,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f415,plain,
n11 = sum(n5,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f416,plain,
n10 = sum(n5,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f417,plain,
n9 = sum(n5,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f418,plain,
n8 = sum(n5,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f419,plain,
n7 = sum(n5,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f420,plain,
n6 = sum(n5,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f421,plain,
n5 = sum(n5,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f422,plain,
n3 = sum(n4,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f423,plain,
n2 = sum(n4,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f424,plain,
n1 = sum(n4,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f425,plain,
n0 = sum(n4,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f426,plain,
n15 = sum(n4,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f427,plain,
n14 = sum(n4,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f428,plain,
n13 = sum(n4,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f429,plain,
n12 = sum(n4,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f430,plain,
n11 = sum(n4,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f431,plain,
n10 = sum(n4,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f432,plain,
n9 = sum(n4,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f433,plain,
n8 = sum(n4,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f434,plain,
n7 = sum(n4,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f435,plain,
n6 = sum(n4,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f436,plain,
n5 = sum(n4,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f437,plain,
n4 = sum(n4,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f438,plain,
n2 = sum(n3,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f439,plain,
n1 = sum(n3,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f440,plain,
n0 = sum(n3,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f441,plain,
n15 = sum(n3,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f442,plain,
n14 = sum(n3,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f443,plain,
n13 = sum(n3,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f444,plain,
n12 = sum(n3,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f445,plain,
n11 = sum(n3,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f446,plain,
n10 = sum(n3,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f447,plain,
n9 = sum(n3,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f448,plain,
n8 = sum(n3,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f449,plain,
n7 = sum(n3,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f450,plain,
n6 = sum(n3,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f451,plain,
n5 = sum(n3,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f452,plain,
n4 = sum(n3,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f453,plain,
n3 = sum(n3,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f454,plain,
n1 = sum(n2,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f455,plain,
n0 = sum(n2,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f456,plain,
n15 = sum(n2,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f457,plain,
n14 = sum(n2,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f458,plain,
n13 = sum(n2,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f459,plain,
n12 = sum(n2,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f460,plain,
n11 = sum(n2,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f461,plain,
n10 = sum(n2,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f462,plain,
n9 = sum(n2,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f463,plain,
n8 = sum(n2,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f464,plain,
n7 = sum(n2,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f465,plain,
n6 = sum(n2,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f466,plain,
n5 = sum(n2,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f467,plain,
n4 = sum(n2,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f468,plain,
n3 = sum(n2,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f469,plain,
n2 = sum(n2,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f470,plain,
n0 = sum(n1,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f471,plain,
n15 = sum(n1,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f472,plain,
n14 = sum(n1,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f473,plain,
n13 = sum(n1,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f474,plain,
n12 = sum(n1,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f475,plain,
n11 = sum(n1,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f476,plain,
n10 = sum(n1,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f477,plain,
n9 = sum(n1,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f478,plain,
n8 = sum(n1,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f479,plain,
n7 = sum(n1,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f480,plain,
n6 = sum(n1,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f481,plain,
n5 = sum(n1,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f482,plain,
n4 = sum(n1,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f483,plain,
n3 = sum(n1,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f484,plain,
n2 = sum(n1,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f485,plain,
n1 = sum(n1,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f486,plain,
n15 = sum(n0,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f487,plain,
n14 = sum(n0,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f488,plain,
n13 = sum(n0,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f489,plain,
n12 = sum(n0,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f490,plain,
n11 = sum(n0,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f491,plain,
n10 = sum(n0,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f492,plain,
n9 = sum(n0,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f493,plain,
n8 = sum(n0,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f494,plain,
n7 = sum(n0,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f495,plain,
n6 = sum(n0,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f496,plain,
n5 = sum(n0,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f497,plain,
n4 = sum(n0,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f498,plain,
n3 = sum(n0,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f499,plain,
n2 = sum(n0,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f500,plain,
n1 = sum(n0,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f501,plain,
n0 = sum(n0,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f502,plain,
n14 = pred(n15),
inference(cnf_transformation,[],[f2]) ).
fof(f503,plain,
n13 = pred(n14),
inference(cnf_transformation,[],[f2]) ).
fof(f504,plain,
n12 = pred(n13),
inference(cnf_transformation,[],[f2]) ).
fof(f505,plain,
n11 = pred(n12),
inference(cnf_transformation,[],[f2]) ).
fof(f506,plain,
n10 = pred(n11),
inference(cnf_transformation,[],[f2]) ).
fof(f507,plain,
n9 = pred(n10),
inference(cnf_transformation,[],[f2]) ).
fof(f508,plain,
n8 = pred(n9),
inference(cnf_transformation,[],[f2]) ).
fof(f509,plain,
n7 = pred(n8),
inference(cnf_transformation,[],[f2]) ).
fof(f510,plain,
n6 = pred(n7),
inference(cnf_transformation,[],[f2]) ).
fof(f511,plain,
n5 = pred(n6),
inference(cnf_transformation,[],[f2]) ).
fof(f512,plain,
n4 = pred(n5),
inference(cnf_transformation,[],[f2]) ).
fof(f513,plain,
n3 = pred(n4),
inference(cnf_transformation,[],[f2]) ).
fof(f514,plain,
n2 = pred(n3),
inference(cnf_transformation,[],[f2]) ).
fof(f515,plain,
n1 = pred(n2),
inference(cnf_transformation,[],[f2]) ).
fof(f516,plain,
n0 = pred(n1),
inference(cnf_transformation,[],[f2]) ).
fof(f517,plain,
n15 = pred(n0),
inference(cnf_transformation,[],[f2]) ).
fof(f518,plain,
n0 = succ(n15),
inference(cnf_transformation,[],[f2]) ).
fof(f519,plain,
succ(n14) = n15,
inference(cnf_transformation,[],[f2]) ).
fof(f520,plain,
succ(n13) = n14,
inference(cnf_transformation,[],[f2]) ).
fof(f521,plain,
succ(n12) = n13,
inference(cnf_transformation,[],[f2]) ).
fof(f522,plain,
succ(n11) = n12,
inference(cnf_transformation,[],[f2]) ).
fof(f523,plain,
succ(n10) = n11,
inference(cnf_transformation,[],[f2]) ).
fof(f524,plain,
succ(n9) = n10,
inference(cnf_transformation,[],[f2]) ).
fof(f525,plain,
succ(n8) = n9,
inference(cnf_transformation,[],[f2]) ).
fof(f526,plain,
succ(n7) = n8,
inference(cnf_transformation,[],[f2]) ).
fof(f527,plain,
succ(n6) = n7,
inference(cnf_transformation,[],[f2]) ).
fof(f528,plain,
succ(n5) = n6,
inference(cnf_transformation,[],[f2]) ).
fof(f529,plain,
succ(n4) = n5,
inference(cnf_transformation,[],[f2]) ).
fof(f530,plain,
succ(n3) = n4,
inference(cnf_transformation,[],[f2]) ).
fof(f531,plain,
succ(n2) = n3,
inference(cnf_transformation,[],[f2]) ).
fof(f532,plain,
succ(n1) = n2,
inference(cnf_transformation,[],[f2]) ).
fof(f533,plain,
succ(n0) = n1,
inference(cnf_transformation,[],[f2]) ).
fof(f1135,definition,
( spl122_121
<=> sK40 = sK41 ),
introduced(definition,[new_symbols(definition,[spl122_121])],[avatar_definition]) ).
fof(f1139,definition,
( spl122_122
<=> sK38 = sK39 ),
introduced(definition,[new_symbols(definition,[spl122_122])],[avatar_definition]) ).
fof(f1143,definition,
( spl122_123
<=> sK36 = sK37 ),
introduced(definition,[new_symbols(definition,[spl122_123])],[avatar_definition]) ).
fof(f1147,definition,
( spl122_124
<=> sK34 = sK35 ),
introduced(definition,[new_symbols(definition,[spl122_124])],[avatar_definition]) ).
fof(f1150,plain,
( ~ spl122_121
| ~ spl122_122
| ~ spl122_123
| ~ spl122_124 ),
inference(avatar_split_clause,[],[f123,f1147,f1143,f1139,f1135]) ).
fof(f1152,definition,
( spl122_125
<=> sK41 = sum(pred(sK120),sum(succ(sK118),sum(pred(sK121),succ(sK119)))) ),
introduced(definition,[new_symbols(definition,[spl122_125])],[avatar_definition]) ).
fof(f1155,plain,
spl122_125,
inference(avatar_split_clause,[],[f124,f1152]) ).
fof(f1157,definition,
( spl122_126
<=> sK40 = sum(sum(pred(sK38),succ(sK39)),sum(pred(sK39),succ(sK38))) ),
introduced(definition,[new_symbols(definition,[spl122_126])],[avatar_definition]) ).
fof(f1160,plain,
spl122_126,
inference(avatar_split_clause,[],[f125,f1157]) ).
fof(f1162,definition,
( spl122_127
<=> sK39 = sum(pred(sK116),sum(succ(sK114),sum(pred(sK117),succ(sK115)))) ),
introduced(definition,[new_symbols(definition,[spl122_127])],[avatar_definition]) ).
fof(f1165,plain,
spl122_127,
inference(avatar_split_clause,[],[f126,f1162]) ).
fof(f1167,definition,
( spl122_128
<=> sK38 = sum(sum(pred(sK36),succ(sK37)),sum(pred(sK37),succ(sK36))) ),
introduced(definition,[new_symbols(definition,[spl122_128])],[avatar_definition]) ).
fof(f1170,plain,
spl122_128,
inference(avatar_split_clause,[],[f127,f1167]) ).
fof(f1172,definition,
( spl122_129
<=> sK37 = sum(pred(sK112),sum(succ(sK110),sum(pred(sK113),succ(sK111)))) ),
introduced(definition,[new_symbols(definition,[spl122_129])],[avatar_definition]) ).
fof(f1175,plain,
spl122_129,
inference(avatar_split_clause,[],[f128,f1172]) ).
fof(f1177,definition,
( spl122_130
<=> sK36 = sum(sum(pred(sK34),succ(sK35)),sum(pred(sK35),succ(sK34))) ),
introduced(definition,[new_symbols(definition,[spl122_130])],[avatar_definition]) ).
fof(f1180,plain,
spl122_130,
inference(avatar_split_clause,[],[f129,f1177]) ).
fof(f1182,definition,
( spl122_131
<=> sK35 = sum(pred(sK108),sum(succ(sK106),sum(pred(sK109),succ(sK107)))) ),
introduced(definition,[new_symbols(definition,[spl122_131])],[avatar_definition]) ).
fof(f1185,plain,
spl122_131,
inference(avatar_split_clause,[],[f130,f1182]) ).
fof(f1187,definition,
( spl122_132
<=> sK34 = sum(sum(pred(sK32),succ(sK33)),sum(pred(sK33),succ(sK32))) ),
introduced(definition,[new_symbols(definition,[spl122_132])],[avatar_definition]) ).
fof(f1190,plain,
spl122_132,
inference(avatar_split_clause,[],[f131,f1187]) ).
fof(f1192,definition,
( spl122_133
<=> sK33 = sum(pred(sK104),sum(succ(sK102),sum(pred(sK105),succ(sK103)))) ),
introduced(definition,[new_symbols(definition,[spl122_133])],[avatar_definition]) ).
fof(f1195,plain,
spl122_133,
inference(avatar_split_clause,[],[f132,f1192]) ).
fof(f1197,definition,
( spl122_134
<=> sK32 = sum(sum(pred(sK30),succ(sK31)),sum(pred(sK31),succ(sK30))) ),
introduced(definition,[new_symbols(definition,[spl122_134])],[avatar_definition]) ).
fof(f1200,plain,
spl122_134,
inference(avatar_split_clause,[],[f133,f1197]) ).
fof(f1202,definition,
( spl122_135
<=> sK31 = sum(pred(sK100),sum(succ(sK98),sum(pred(sK101),succ(sK99)))) ),
introduced(definition,[new_symbols(definition,[spl122_135])],[avatar_definition]) ).
fof(f1205,plain,
spl122_135,
inference(avatar_split_clause,[],[f134,f1202]) ).
fof(f1207,definition,
( spl122_136
<=> sK30 = sum(sum(pred(sK28),succ(sK29)),sum(pred(sK29),succ(sK28))) ),
introduced(definition,[new_symbols(definition,[spl122_136])],[avatar_definition]) ).
fof(f1210,plain,
spl122_136,
inference(avatar_split_clause,[],[f135,f1207]) ).
fof(f1212,definition,
( spl122_137
<=> sK29 = sum(pred(sK96),sum(succ(sK94),sum(pred(sK97),succ(sK95)))) ),
introduced(definition,[new_symbols(definition,[spl122_137])],[avatar_definition]) ).
fof(f1215,plain,
spl122_137,
inference(avatar_split_clause,[],[f136,f1212]) ).
fof(f1217,definition,
( spl122_138
<=> sK28 = sum(sum(pred(sK26),succ(sK27)),sum(pred(sK27),succ(sK26))) ),
introduced(definition,[new_symbols(definition,[spl122_138])],[avatar_definition]) ).
fof(f1220,plain,
spl122_138,
inference(avatar_split_clause,[],[f137,f1217]) ).
fof(f1222,definition,
( spl122_139
<=> sK27 = sum(pred(sK92),sum(succ(sK90),sum(pred(sK93),succ(sK91)))) ),
introduced(definition,[new_symbols(definition,[spl122_139])],[avatar_definition]) ).
fof(f1225,plain,
spl122_139,
inference(avatar_split_clause,[],[f138,f1222]) ).
fof(f1227,definition,
( spl122_140
<=> sK26 = sum(sum(pred(sK24),succ(sK25)),sum(pred(sK25),succ(sK24))) ),
introduced(definition,[new_symbols(definition,[spl122_140])],[avatar_definition]) ).
fof(f1230,plain,
spl122_140,
inference(avatar_split_clause,[],[f139,f1227]) ).
fof(f1232,definition,
( spl122_141
<=> sK25 = sum(pred(sK88),sum(succ(sK86),sum(pred(sK89),succ(sK87)))) ),
introduced(definition,[new_symbols(definition,[spl122_141])],[avatar_definition]) ).
fof(f1235,plain,
spl122_141,
inference(avatar_split_clause,[],[f140,f1232]) ).
fof(f1237,definition,
( spl122_142
<=> sK24 = sum(sum(pred(sK22),succ(sK23)),sum(pred(sK23),succ(sK22))) ),
introduced(definition,[new_symbols(definition,[spl122_142])],[avatar_definition]) ).
fof(f1240,plain,
spl122_142,
inference(avatar_split_clause,[],[f141,f1237]) ).
fof(f1242,definition,
( spl122_143
<=> sK23 = sum(pred(sK84),sum(succ(sK82),sum(pred(sK85),succ(sK83)))) ),
introduced(definition,[new_symbols(definition,[spl122_143])],[avatar_definition]) ).
fof(f1245,plain,
spl122_143,
inference(avatar_split_clause,[],[f142,f1242]) ).
fof(f1247,definition,
( spl122_144
<=> sK22 = sum(sum(pred(sK20),succ(sK21)),sum(pred(sK21),succ(sK20))) ),
introduced(definition,[new_symbols(definition,[spl122_144])],[avatar_definition]) ).
fof(f1250,plain,
spl122_144,
inference(avatar_split_clause,[],[f143,f1247]) ).
fof(f1252,definition,
( spl122_145
<=> sK21 = sum(pred(sK80),sum(succ(sK78),sum(pred(sK81),succ(sK79)))) ),
introduced(definition,[new_symbols(definition,[spl122_145])],[avatar_definition]) ).
fof(f1255,plain,
spl122_145,
inference(avatar_split_clause,[],[f144,f1252]) ).
fof(f1257,definition,
( spl122_146
<=> sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18))) ),
introduced(definition,[new_symbols(definition,[spl122_146])],[avatar_definition]) ).
fof(f1260,plain,
spl122_146,
inference(avatar_split_clause,[],[f145,f1257]) ).
fof(f1262,definition,
( spl122_147
<=> sK19 = sum(pred(sK76),sum(succ(sK74),sum(pred(sK77),succ(sK75)))) ),
introduced(definition,[new_symbols(definition,[spl122_147])],[avatar_definition]) ).
fof(f1265,plain,
spl122_147,
inference(avatar_split_clause,[],[f146,f1262]) ).
fof(f1267,definition,
( spl122_148
<=> sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16))) ),
introduced(definition,[new_symbols(definition,[spl122_148])],[avatar_definition]) ).
fof(f1270,plain,
spl122_148,
inference(avatar_split_clause,[],[f147,f1267]) ).
fof(f1272,definition,
( spl122_149
<=> sK17 = sum(pred(sK72),sum(succ(sK70),sum(pred(sK73),succ(sK71)))) ),
introduced(definition,[new_symbols(definition,[spl122_149])],[avatar_definition]) ).
fof(f1275,plain,
spl122_149,
inference(avatar_split_clause,[],[f148,f1272]) ).
fof(f1277,definition,
( spl122_150
<=> sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14))) ),
introduced(definition,[new_symbols(definition,[spl122_150])],[avatar_definition]) ).
fof(f1280,plain,
spl122_150,
inference(avatar_split_clause,[],[f149,f1277]) ).
fof(f1282,definition,
( spl122_151
<=> sK15 = sum(pred(sK68),sum(succ(sK66),sum(pred(sK69),succ(sK67)))) ),
introduced(definition,[new_symbols(definition,[spl122_151])],[avatar_definition]) ).
fof(f1285,plain,
spl122_151,
inference(avatar_split_clause,[],[f150,f1282]) ).
fof(f1287,definition,
( spl122_152
<=> sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12))) ),
introduced(definition,[new_symbols(definition,[spl122_152])],[avatar_definition]) ).
fof(f1290,plain,
spl122_152,
inference(avatar_split_clause,[],[f151,f1287]) ).
fof(f1292,definition,
( spl122_153
<=> sK13 = sum(pred(sK64),sum(succ(sK62),sum(pred(sK65),succ(sK63)))) ),
introduced(definition,[new_symbols(definition,[spl122_153])],[avatar_definition]) ).
fof(f1295,plain,
spl122_153,
inference(avatar_split_clause,[],[f152,f1292]) ).
fof(f1297,definition,
( spl122_154
<=> sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10))) ),
introduced(definition,[new_symbols(definition,[spl122_154])],[avatar_definition]) ).
fof(f1300,plain,
spl122_154,
inference(avatar_split_clause,[],[f153,f1297]) ).
fof(f1302,definition,
( spl122_155
<=> sK11 = sum(pred(sK60),sum(succ(sK58),sum(pred(sK61),succ(sK59)))) ),
introduced(definition,[new_symbols(definition,[spl122_155])],[avatar_definition]) ).
fof(f1305,plain,
spl122_155,
inference(avatar_split_clause,[],[f154,f1302]) ).
fof(f1307,definition,
( spl122_156
<=> sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8))) ),
introduced(definition,[new_symbols(definition,[spl122_156])],[avatar_definition]) ).
fof(f1310,plain,
spl122_156,
inference(avatar_split_clause,[],[f155,f1307]) ).
fof(f1312,definition,
( spl122_157
<=> sK9 = sum(pred(sK56),sum(succ(sK54),sum(pred(sK57),succ(sK55)))) ),
introduced(definition,[new_symbols(definition,[spl122_157])],[avatar_definition]) ).
fof(f1315,plain,
spl122_157,
inference(avatar_split_clause,[],[f156,f1312]) ).
fof(f1317,definition,
( spl122_158
<=> sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6))) ),
introduced(definition,[new_symbols(definition,[spl122_158])],[avatar_definition]) ).
fof(f1320,plain,
spl122_158,
inference(avatar_split_clause,[],[f157,f1317]) ).
fof(f1322,definition,
( spl122_159
<=> sK7 = sum(pred(sK52),sum(succ(sK50),sum(pred(sK53),succ(sK51)))) ),
introduced(definition,[new_symbols(definition,[spl122_159])],[avatar_definition]) ).
fof(f1325,plain,
spl122_159,
inference(avatar_split_clause,[],[f158,f1322]) ).
fof(f1327,definition,
( spl122_160
<=> sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4))) ),
introduced(definition,[new_symbols(definition,[spl122_160])],[avatar_definition]) ).
fof(f1330,plain,
spl122_160,
inference(avatar_split_clause,[],[f159,f1327]) ).
fof(f1332,definition,
( spl122_161
<=> sK5 = sum(pred(sK48),sum(succ(sK46),sum(pred(sK49),succ(sK47)))) ),
introduced(definition,[new_symbols(definition,[spl122_161])],[avatar_definition]) ).
fof(f1335,plain,
spl122_161,
inference(avatar_split_clause,[],[f160,f1332]) ).
fof(f1337,definition,
( spl122_162
<=> sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2))) ),
introduced(definition,[new_symbols(definition,[spl122_162])],[avatar_definition]) ).
fof(f1340,plain,
spl122_162,
inference(avatar_split_clause,[],[f161,f1337]) ).
fof(f1342,definition,
( spl122_163
<=> sK3 = sum(pred(sK44),sum(succ(sK42),sum(pred(sK45),succ(sK43)))) ),
introduced(definition,[new_symbols(definition,[spl122_163])],[avatar_definition]) ).
fof(f1345,plain,
spl122_163,
inference(avatar_split_clause,[],[f162,f1342]) ).
fof(f1347,definition,
( spl122_164
<=> sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0))) ),
introduced(definition,[new_symbols(definition,[spl122_164])],[avatar_definition]) ).
fof(f1350,plain,
spl122_164,
inference(avatar_split_clause,[],[f163,f1347]) ).
fof(f1352,definition,
( spl122_165
<=> sK121 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK39)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_165])],[avatar_definition]) ).
fof(f1355,plain,
spl122_165,
inference(avatar_split_clause,[],[f164,f1352]) ).
fof(f1357,definition,
( spl122_166
<=> sK119 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK39)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_166])],[avatar_definition]) ).
fof(f1360,plain,
spl122_166,
inference(avatar_split_clause,[],[f165,f1357]) ).
fof(f1362,definition,
( spl122_167
<=> sK120 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK38)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_167])],[avatar_definition]) ).
fof(f1365,plain,
spl122_167,
inference(avatar_split_clause,[],[f166,f1362]) ).
fof(f1367,definition,
( spl122_168
<=> sK118 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK38)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_168])],[avatar_definition]) ).
fof(f1370,plain,
spl122_168,
inference(avatar_split_clause,[],[f167,f1367]) ).
fof(f1372,definition,
( spl122_169
<=> sK117 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK37)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_169])],[avatar_definition]) ).
fof(f1375,plain,
spl122_169,
inference(avatar_split_clause,[],[f168,f1372]) ).
fof(f1377,definition,
( spl122_170
<=> sK115 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK37)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_170])],[avatar_definition]) ).
fof(f1380,plain,
spl122_170,
inference(avatar_split_clause,[],[f169,f1377]) ).
fof(f1382,definition,
( spl122_171
<=> sK116 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK36)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_171])],[avatar_definition]) ).
fof(f1385,plain,
spl122_171,
inference(avatar_split_clause,[],[f170,f1382]) ).
fof(f1387,definition,
( spl122_172
<=> sK114 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK36)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_172])],[avatar_definition]) ).
fof(f1390,plain,
spl122_172,
inference(avatar_split_clause,[],[f171,f1387]) ).
fof(f1392,definition,
( spl122_173
<=> sK113 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK35)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_173])],[avatar_definition]) ).
fof(f1395,plain,
spl122_173,
inference(avatar_split_clause,[],[f172,f1392]) ).
fof(f1397,definition,
( spl122_174
<=> sK111 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK35)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_174])],[avatar_definition]) ).
fof(f1400,plain,
spl122_174,
inference(avatar_split_clause,[],[f173,f1397]) ).
fof(f1402,definition,
( spl122_175
<=> sK112 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK34)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_175])],[avatar_definition]) ).
fof(f1405,plain,
spl122_175,
inference(avatar_split_clause,[],[f174,f1402]) ).
fof(f1407,definition,
( spl122_176
<=> sK110 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK34)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_176])],[avatar_definition]) ).
fof(f1410,plain,
spl122_176,
inference(avatar_split_clause,[],[f175,f1407]) ).
fof(f1412,definition,
( spl122_177
<=> sK109 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK33)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_177])],[avatar_definition]) ).
fof(f1415,plain,
spl122_177,
inference(avatar_split_clause,[],[f176,f1412]) ).
fof(f1417,definition,
( spl122_178
<=> sK107 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK33)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_178])],[avatar_definition]) ).
fof(f1420,plain,
spl122_178,
inference(avatar_split_clause,[],[f177,f1417]) ).
fof(f1422,definition,
( spl122_179
<=> sK108 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK32)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_179])],[avatar_definition]) ).
fof(f1425,plain,
spl122_179,
inference(avatar_split_clause,[],[f178,f1422]) ).
fof(f1427,definition,
( spl122_180
<=> sK106 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK32)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_180])],[avatar_definition]) ).
fof(f1430,plain,
spl122_180,
inference(avatar_split_clause,[],[f179,f1427]) ).
fof(f1432,definition,
( spl122_181
<=> sK105 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK31)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_181])],[avatar_definition]) ).
fof(f1435,plain,
spl122_181,
inference(avatar_split_clause,[],[f180,f1432]) ).
fof(f1437,definition,
( spl122_182
<=> sK103 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK31)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_182])],[avatar_definition]) ).
fof(f1440,plain,
spl122_182,
inference(avatar_split_clause,[],[f181,f1437]) ).
fof(f1442,definition,
( spl122_183
<=> sK104 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK30)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_183])],[avatar_definition]) ).
fof(f1445,plain,
spl122_183,
inference(avatar_split_clause,[],[f182,f1442]) ).
fof(f1447,definition,
( spl122_184
<=> sK102 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK30)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_184])],[avatar_definition]) ).
fof(f1450,plain,
spl122_184,
inference(avatar_split_clause,[],[f183,f1447]) ).
fof(f1452,definition,
( spl122_185
<=> sK101 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK29)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_185])],[avatar_definition]) ).
fof(f1455,plain,
spl122_185,
inference(avatar_split_clause,[],[f184,f1452]) ).
fof(f1457,definition,
( spl122_186
<=> sK99 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK29)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_186])],[avatar_definition]) ).
fof(f1460,plain,
spl122_186,
inference(avatar_split_clause,[],[f185,f1457]) ).
fof(f1462,definition,
( spl122_187
<=> sK100 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK28)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_187])],[avatar_definition]) ).
fof(f1465,plain,
spl122_187,
inference(avatar_split_clause,[],[f186,f1462]) ).
fof(f1467,definition,
( spl122_188
<=> sK98 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK28)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_188])],[avatar_definition]) ).
fof(f1470,plain,
spl122_188,
inference(avatar_split_clause,[],[f187,f1467]) ).
fof(f1472,definition,
( spl122_189
<=> sK97 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK27)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_189])],[avatar_definition]) ).
fof(f1475,plain,
spl122_189,
inference(avatar_split_clause,[],[f188,f1472]) ).
fof(f1477,definition,
( spl122_190
<=> sK95 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK27)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_190])],[avatar_definition]) ).
fof(f1480,plain,
spl122_190,
inference(avatar_split_clause,[],[f189,f1477]) ).
fof(f1482,definition,
( spl122_191
<=> sK96 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK26)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_191])],[avatar_definition]) ).
fof(f1485,plain,
spl122_191,
inference(avatar_split_clause,[],[f190,f1482]) ).
fof(f1487,definition,
( spl122_192
<=> sK94 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK26)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_192])],[avatar_definition]) ).
fof(f1490,plain,
spl122_192,
inference(avatar_split_clause,[],[f191,f1487]) ).
fof(f1492,definition,
( spl122_193
<=> sK93 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK25)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_193])],[avatar_definition]) ).
fof(f1495,plain,
spl122_193,
inference(avatar_split_clause,[],[f192,f1492]) ).
fof(f1497,definition,
( spl122_194
<=> sK91 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK25)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_194])],[avatar_definition]) ).
fof(f1500,plain,
spl122_194,
inference(avatar_split_clause,[],[f193,f1497]) ).
fof(f1502,definition,
( spl122_195
<=> sK92 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK24)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_195])],[avatar_definition]) ).
fof(f1505,plain,
spl122_195,
inference(avatar_split_clause,[],[f194,f1502]) ).
fof(f1507,definition,
( spl122_196
<=> sK90 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK24)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_196])],[avatar_definition]) ).
fof(f1510,plain,
spl122_196,
inference(avatar_split_clause,[],[f195,f1507]) ).
fof(f1512,definition,
( spl122_197
<=> sK89 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK23)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_197])],[avatar_definition]) ).
fof(f1515,plain,
spl122_197,
inference(avatar_split_clause,[],[f196,f1512]) ).
fof(f1517,definition,
( spl122_198
<=> sK87 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK23)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_198])],[avatar_definition]) ).
fof(f1520,plain,
spl122_198,
inference(avatar_split_clause,[],[f197,f1517]) ).
fof(f1522,definition,
( spl122_199
<=> sK88 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK22)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_199])],[avatar_definition]) ).
fof(f1525,plain,
spl122_199,
inference(avatar_split_clause,[],[f198,f1522]) ).
fof(f1527,definition,
( spl122_200
<=> sK86 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK22)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_200])],[avatar_definition]) ).
fof(f1530,plain,
spl122_200,
inference(avatar_split_clause,[],[f199,f1527]) ).
fof(f1532,definition,
( spl122_201
<=> sK85 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK21)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_201])],[avatar_definition]) ).
fof(f1535,plain,
spl122_201,
inference(avatar_split_clause,[],[f200,f1532]) ).
fof(f1537,definition,
( spl122_202
<=> sK83 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK21)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_202])],[avatar_definition]) ).
fof(f1540,plain,
spl122_202,
inference(avatar_split_clause,[],[f201,f1537]) ).
fof(f1542,definition,
( spl122_203
<=> sK84 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK20)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_203])],[avatar_definition]) ).
fof(f1545,plain,
spl122_203,
inference(avatar_split_clause,[],[f202,f1542]) ).
fof(f1547,definition,
( spl122_204
<=> sK82 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK20)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_204])],[avatar_definition]) ).
fof(f1550,plain,
spl122_204,
inference(avatar_split_clause,[],[f203,f1547]) ).
fof(f1552,definition,
( spl122_205
<=> sK81 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK19)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_205])],[avatar_definition]) ).
fof(f1555,plain,
spl122_205,
inference(avatar_split_clause,[],[f204,f1552]) ).
fof(f1557,definition,
( spl122_206
<=> sK79 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK19)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_206])],[avatar_definition]) ).
fof(f1560,plain,
spl122_206,
inference(avatar_split_clause,[],[f205,f1557]) ).
fof(f1562,definition,
( spl122_207
<=> sK80 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK18)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_207])],[avatar_definition]) ).
fof(f1565,plain,
spl122_207,
inference(avatar_split_clause,[],[f206,f1562]) ).
fof(f1567,definition,
( spl122_208
<=> sK78 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK18)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_208])],[avatar_definition]) ).
fof(f1570,plain,
spl122_208,
inference(avatar_split_clause,[],[f207,f1567]) ).
fof(f1572,definition,
( spl122_209
<=> sK77 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK17)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_209])],[avatar_definition]) ).
fof(f1575,plain,
spl122_209,
inference(avatar_split_clause,[],[f208,f1572]) ).
fof(f1577,definition,
( spl122_210
<=> sK75 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK17)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_210])],[avatar_definition]) ).
fof(f1580,plain,
spl122_210,
inference(avatar_split_clause,[],[f209,f1577]) ).
fof(f1582,definition,
( spl122_211
<=> sK76 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK16)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_211])],[avatar_definition]) ).
fof(f1585,plain,
spl122_211,
inference(avatar_split_clause,[],[f210,f1582]) ).
fof(f1587,definition,
( spl122_212
<=> sK74 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK16)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_212])],[avatar_definition]) ).
fof(f1590,plain,
spl122_212,
inference(avatar_split_clause,[],[f211,f1587]) ).
fof(f1592,definition,
( spl122_213
<=> sK73 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK15)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_213])],[avatar_definition]) ).
fof(f1595,plain,
spl122_213,
inference(avatar_split_clause,[],[f212,f1592]) ).
fof(f1597,definition,
( spl122_214
<=> sK71 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK15)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_214])],[avatar_definition]) ).
fof(f1600,plain,
spl122_214,
inference(avatar_split_clause,[],[f213,f1597]) ).
fof(f1602,definition,
( spl122_215
<=> sK72 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK14)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_215])],[avatar_definition]) ).
fof(f1605,plain,
spl122_215,
inference(avatar_split_clause,[],[f214,f1602]) ).
fof(f1607,definition,
( spl122_216
<=> sK70 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK14)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_216])],[avatar_definition]) ).
fof(f1610,plain,
spl122_216,
inference(avatar_split_clause,[],[f215,f1607]) ).
fof(f1612,definition,
( spl122_217
<=> sK69 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK13)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_217])],[avatar_definition]) ).
fof(f1615,plain,
spl122_217,
inference(avatar_split_clause,[],[f216,f1612]) ).
fof(f1617,definition,
( spl122_218
<=> sK67 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK13)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_218])],[avatar_definition]) ).
fof(f1620,plain,
spl122_218,
inference(avatar_split_clause,[],[f217,f1617]) ).
fof(f1622,definition,
( spl122_219
<=> sK68 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK12)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_219])],[avatar_definition]) ).
fof(f1625,plain,
spl122_219,
inference(avatar_split_clause,[],[f218,f1622]) ).
fof(f1627,definition,
( spl122_220
<=> sK66 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK12)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_220])],[avatar_definition]) ).
fof(f1630,plain,
spl122_220,
inference(avatar_split_clause,[],[f219,f1627]) ).
fof(f1632,definition,
( spl122_221
<=> sK65 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK11)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_221])],[avatar_definition]) ).
fof(f1635,plain,
spl122_221,
inference(avatar_split_clause,[],[f220,f1632]) ).
fof(f1637,definition,
( spl122_222
<=> sK63 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK11)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_222])],[avatar_definition]) ).
fof(f1640,plain,
spl122_222,
inference(avatar_split_clause,[],[f221,f1637]) ).
fof(f1642,definition,
( spl122_223
<=> sK64 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK10)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_223])],[avatar_definition]) ).
fof(f1645,plain,
spl122_223,
inference(avatar_split_clause,[],[f222,f1642]) ).
fof(f1647,definition,
( spl122_224
<=> sK62 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK10)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_224])],[avatar_definition]) ).
fof(f1650,plain,
spl122_224,
inference(avatar_split_clause,[],[f223,f1647]) ).
fof(f1652,definition,
( spl122_225
<=> sK61 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK9)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_225])],[avatar_definition]) ).
fof(f1655,plain,
spl122_225,
inference(avatar_split_clause,[],[f224,f1652]) ).
fof(f1657,definition,
( spl122_226
<=> sK59 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK9)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_226])],[avatar_definition]) ).
fof(f1660,plain,
spl122_226,
inference(avatar_split_clause,[],[f225,f1657]) ).
fof(f1662,definition,
( spl122_227
<=> sK60 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK8)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_227])],[avatar_definition]) ).
fof(f1665,plain,
spl122_227,
inference(avatar_split_clause,[],[f226,f1662]) ).
fof(f1667,definition,
( spl122_228
<=> sK58 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK8)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_228])],[avatar_definition]) ).
fof(f1670,plain,
spl122_228,
inference(avatar_split_clause,[],[f227,f1667]) ).
fof(f1672,definition,
( spl122_229
<=> sK57 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK7)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_229])],[avatar_definition]) ).
fof(f1675,plain,
spl122_229,
inference(avatar_split_clause,[],[f228,f1672]) ).
fof(f1677,definition,
( spl122_230
<=> sK55 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK7)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_230])],[avatar_definition]) ).
fof(f1680,plain,
spl122_230,
inference(avatar_split_clause,[],[f229,f1677]) ).
fof(f1682,definition,
( spl122_231
<=> sK56 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK6)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_231])],[avatar_definition]) ).
fof(f1685,plain,
spl122_231,
inference(avatar_split_clause,[],[f230,f1682]) ).
fof(f1687,definition,
( spl122_232
<=> sK54 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK6)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_232])],[avatar_definition]) ).
fof(f1690,plain,
spl122_232,
inference(avatar_split_clause,[],[f231,f1687]) ).
fof(f1692,definition,
( spl122_233
<=> sK53 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK5)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_233])],[avatar_definition]) ).
fof(f1695,plain,
spl122_233,
inference(avatar_split_clause,[],[f232,f1692]) ).
fof(f1697,definition,
( spl122_234
<=> sK51 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK5)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_234])],[avatar_definition]) ).
fof(f1700,plain,
spl122_234,
inference(avatar_split_clause,[],[f233,f1697]) ).
fof(f1702,definition,
( spl122_235
<=> sK52 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK4)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_235])],[avatar_definition]) ).
fof(f1705,plain,
spl122_235,
inference(avatar_split_clause,[],[f234,f1702]) ).
fof(f1707,definition,
( spl122_236
<=> sK50 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK4)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_236])],[avatar_definition]) ).
fof(f1710,plain,
spl122_236,
inference(avatar_split_clause,[],[f235,f1707]) ).
fof(f1712,definition,
( spl122_237
<=> sK49 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK3)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_237])],[avatar_definition]) ).
fof(f1715,plain,
spl122_237,
inference(avatar_split_clause,[],[f236,f1712]) ).
fof(f1717,definition,
( spl122_238
<=> sK47 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK3)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_238])],[avatar_definition]) ).
fof(f1720,plain,
spl122_238,
inference(avatar_split_clause,[],[f237,f1717]) ).
fof(f1722,definition,
( spl122_239
<=> sK48 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK2)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_239])],[avatar_definition]) ).
fof(f1725,plain,
spl122_239,
inference(avatar_split_clause,[],[f238,f1722]) ).
fof(f1727,definition,
( spl122_240
<=> sK46 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK2)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_240])],[avatar_definition]) ).
fof(f1730,plain,
spl122_240,
inference(avatar_split_clause,[],[f239,f1727]) ).
fof(f1732,definition,
( spl122_241
<=> sK45 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK1)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_241])],[avatar_definition]) ).
fof(f1735,plain,
spl122_241,
inference(avatar_split_clause,[],[f240,f1732]) ).
fof(f1737,definition,
( spl122_242
<=> sK43 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK1)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_242])],[avatar_definition]) ).
fof(f1740,plain,
spl122_242,
inference(avatar_split_clause,[],[f241,f1737]) ).
fof(f1742,definition,
( spl122_243
<=> sK44 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK0)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_243])],[avatar_definition]) ).
fof(f1745,plain,
spl122_243,
inference(avatar_split_clause,[],[f242,f1742]) ).
fof(f1747,definition,
( spl122_244
<=> sK42 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK0)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl122_244])],[avatar_definition]) ).
fof(f1750,plain,
spl122_244,
inference(avatar_split_clause,[],[f243,f1747]) ).
fof(f1752,definition,
( spl122_245
<=> n15 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_245])],[avatar_definition]) ).
fof(f1756,definition,
( spl122_246
<=> n14 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_246])],[avatar_definition]) ).
fof(f1760,definition,
( spl122_247
<=> n13 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_247])],[avatar_definition]) ).
fof(f1764,definition,
( spl122_248
<=> n12 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_248])],[avatar_definition]) ).
fof(f1768,definition,
( spl122_249
<=> n11 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_249])],[avatar_definition]) ).
fof(f1772,definition,
( spl122_250
<=> n10 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_250])],[avatar_definition]) ).
fof(f1776,definition,
( spl122_251
<=> n9 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_251])],[avatar_definition]) ).
fof(f1780,definition,
( spl122_252
<=> n8 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_252])],[avatar_definition]) ).
fof(f1784,definition,
( spl122_253
<=> n7 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_253])],[avatar_definition]) ).
fof(f1788,definition,
( spl122_254
<=> n6 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_254])],[avatar_definition]) ).
fof(f1792,definition,
( spl122_255
<=> n5 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_255])],[avatar_definition]) ).
fof(f1796,definition,
( spl122_256
<=> n4 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_256])],[avatar_definition]) ).
fof(f1800,definition,
( spl122_257
<=> n3 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_257])],[avatar_definition]) ).
fof(f1804,definition,
( spl122_258
<=> n2 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_258])],[avatar_definition]) ).
fof(f1808,definition,
( spl122_259
<=> n1 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_259])],[avatar_definition]) ).
fof(f1812,definition,
( spl122_260
<=> n0 = sK1 ),
introduced(definition,[new_symbols(definition,[spl122_260])],[avatar_definition]) ).
fof(f1815,plain,
( spl122_245
| spl122_246
| spl122_247
| spl122_248
| spl122_249
| spl122_250
| spl122_251
| spl122_252
| spl122_253
| spl122_254
| spl122_255
| spl122_256
| spl122_257
| spl122_258
| spl122_259
| spl122_260 ),
inference(avatar_split_clause,[],[f244,f1812,f1808,f1804,f1800,f1796,f1792,f1788,f1784,f1780,f1776,f1772,f1768,f1764,f1760,f1756,f1752]) ).
fof(f1817,definition,
( spl122_261
<=> n15 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_261])],[avatar_definition]) ).
fof(f1821,definition,
( spl122_262
<=> n14 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_262])],[avatar_definition]) ).
fof(f1825,definition,
( spl122_263
<=> n13 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_263])],[avatar_definition]) ).
fof(f1829,definition,
( spl122_264
<=> n12 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_264])],[avatar_definition]) ).
fof(f1833,definition,
( spl122_265
<=> n11 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_265])],[avatar_definition]) ).
fof(f1837,definition,
( spl122_266
<=> n10 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_266])],[avatar_definition]) ).
fof(f1841,definition,
( spl122_267
<=> n9 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_267])],[avatar_definition]) ).
fof(f1845,definition,
( spl122_268
<=> n8 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_268])],[avatar_definition]) ).
fof(f1849,definition,
( spl122_269
<=> n7 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_269])],[avatar_definition]) ).
fof(f1853,definition,
( spl122_270
<=> n6 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_270])],[avatar_definition]) ).
fof(f1857,definition,
( spl122_271
<=> n5 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_271])],[avatar_definition]) ).
fof(f1861,definition,
( spl122_272
<=> n4 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_272])],[avatar_definition]) ).
fof(f1865,definition,
( spl122_273
<=> n3 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_273])],[avatar_definition]) ).
fof(f1869,definition,
( spl122_274
<=> n2 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_274])],[avatar_definition]) ).
fof(f1873,definition,
( spl122_275
<=> n1 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_275])],[avatar_definition]) ).
fof(f1877,definition,
( spl122_276
<=> n0 = sK0 ),
introduced(definition,[new_symbols(definition,[spl122_276])],[avatar_definition]) ).
fof(f1880,plain,
( spl122_261
| spl122_262
| spl122_263
| spl122_264
| spl122_265
| spl122_266
| spl122_267
| spl122_268
| spl122_269
| spl122_270
| spl122_271
| spl122_272
| spl122_273
| spl122_274
| spl122_275
| spl122_276 ),
inference(avatar_split_clause,[],[f245,f1877,f1873,f1869,f1865,f1861,f1857,f1853,f1849,f1845,f1841,f1837,f1833,f1829,f1825,f1821,f1817]) ).
fof(f1882,definition,
( spl122_277
<=> n14 = sum(n15,n15) ),
introduced(definition,[new_symbols(definition,[spl122_277])],[avatar_definition]) ).
fof(f1885,plain,
spl122_277,
inference(avatar_split_clause,[],[f246,f1882]) ).
fof(f1887,definition,
( spl122_278
<=> n13 = sum(n15,n14) ),
introduced(definition,[new_symbols(definition,[spl122_278])],[avatar_definition]) ).
fof(f1890,plain,
spl122_278,
inference(avatar_split_clause,[],[f247,f1887]) ).
fof(f1892,definition,
( spl122_279
<=> n12 = sum(n15,n13) ),
introduced(definition,[new_symbols(definition,[spl122_279])],[avatar_definition]) ).
fof(f1895,plain,
spl122_279,
inference(avatar_split_clause,[],[f248,f1892]) ).
fof(f1897,definition,
( spl122_280
<=> n11 = sum(n15,n12) ),
introduced(definition,[new_symbols(definition,[spl122_280])],[avatar_definition]) ).
fof(f1900,plain,
spl122_280,
inference(avatar_split_clause,[],[f249,f1897]) ).
fof(f1902,definition,
( spl122_281
<=> n10 = sum(n15,n11) ),
introduced(definition,[new_symbols(definition,[spl122_281])],[avatar_definition]) ).
fof(f1905,plain,
spl122_281,
inference(avatar_split_clause,[],[f250,f1902]) ).
fof(f1907,definition,
( spl122_282
<=> n9 = sum(n15,n10) ),
introduced(definition,[new_symbols(definition,[spl122_282])],[avatar_definition]) ).
fof(f1910,plain,
spl122_282,
inference(avatar_split_clause,[],[f251,f1907]) ).
fof(f1912,definition,
( spl122_283
<=> n8 = sum(n15,n9) ),
introduced(definition,[new_symbols(definition,[spl122_283])],[avatar_definition]) ).
fof(f1915,plain,
spl122_283,
inference(avatar_split_clause,[],[f252,f1912]) ).
fof(f1917,definition,
( spl122_284
<=> n7 = sum(n15,n8) ),
introduced(definition,[new_symbols(definition,[spl122_284])],[avatar_definition]) ).
fof(f1920,plain,
spl122_284,
inference(avatar_split_clause,[],[f253,f1917]) ).
fof(f1922,definition,
( spl122_285
<=> n6 = sum(n15,n7) ),
introduced(definition,[new_symbols(definition,[spl122_285])],[avatar_definition]) ).
fof(f1925,plain,
spl122_285,
inference(avatar_split_clause,[],[f254,f1922]) ).
fof(f1927,definition,
( spl122_286
<=> n5 = sum(n15,n6) ),
introduced(definition,[new_symbols(definition,[spl122_286])],[avatar_definition]) ).
fof(f1930,plain,
spl122_286,
inference(avatar_split_clause,[],[f255,f1927]) ).
fof(f1932,definition,
( spl122_287
<=> n4 = sum(n15,n5) ),
introduced(definition,[new_symbols(definition,[spl122_287])],[avatar_definition]) ).
fof(f1935,plain,
spl122_287,
inference(avatar_split_clause,[],[f256,f1932]) ).
fof(f1937,definition,
( spl122_288
<=> n3 = sum(n15,n4) ),
introduced(definition,[new_symbols(definition,[spl122_288])],[avatar_definition]) ).
fof(f1940,plain,
spl122_288,
inference(avatar_split_clause,[],[f257,f1937]) ).
fof(f1942,definition,
( spl122_289
<=> n2 = sum(n15,n3) ),
introduced(definition,[new_symbols(definition,[spl122_289])],[avatar_definition]) ).
fof(f1945,plain,
spl122_289,
inference(avatar_split_clause,[],[f258,f1942]) ).
fof(f1947,definition,
( spl122_290
<=> n1 = sum(n15,n2) ),
introduced(definition,[new_symbols(definition,[spl122_290])],[avatar_definition]) ).
fof(f1950,plain,
spl122_290,
inference(avatar_split_clause,[],[f259,f1947]) ).
fof(f1952,definition,
( spl122_291
<=> n0 = sum(n15,n1) ),
introduced(definition,[new_symbols(definition,[spl122_291])],[avatar_definition]) ).
fof(f1955,plain,
spl122_291,
inference(avatar_split_clause,[],[f260,f1952]) ).
fof(f1957,definition,
( spl122_292
<=> n15 = sum(n15,n0) ),
introduced(definition,[new_symbols(definition,[spl122_292])],[avatar_definition]) ).
fof(f1960,plain,
spl122_292,
inference(avatar_split_clause,[],[f261,f1957]) ).
fof(f1962,definition,
( spl122_293
<=> n13 = sum(n14,n15) ),
introduced(definition,[new_symbols(definition,[spl122_293])],[avatar_definition]) ).
fof(f1965,plain,
spl122_293,
inference(avatar_split_clause,[],[f262,f1962]) ).
fof(f1967,definition,
( spl122_294
<=> n12 = sum(n14,n14) ),
introduced(definition,[new_symbols(definition,[spl122_294])],[avatar_definition]) ).
fof(f1970,plain,
spl122_294,
inference(avatar_split_clause,[],[f263,f1967]) ).
fof(f1972,definition,
( spl122_295
<=> n11 = sum(n14,n13) ),
introduced(definition,[new_symbols(definition,[spl122_295])],[avatar_definition]) ).
fof(f1975,plain,
spl122_295,
inference(avatar_split_clause,[],[f264,f1972]) ).
fof(f1977,definition,
( spl122_296
<=> n10 = sum(n14,n12) ),
introduced(definition,[new_symbols(definition,[spl122_296])],[avatar_definition]) ).
fof(f1980,plain,
spl122_296,
inference(avatar_split_clause,[],[f265,f1977]) ).
fof(f1982,definition,
( spl122_297
<=> n9 = sum(n14,n11) ),
introduced(definition,[new_symbols(definition,[spl122_297])],[avatar_definition]) ).
fof(f1985,plain,
spl122_297,
inference(avatar_split_clause,[],[f266,f1982]) ).
fof(f1987,definition,
( spl122_298
<=> n8 = sum(n14,n10) ),
introduced(definition,[new_symbols(definition,[spl122_298])],[avatar_definition]) ).
fof(f1990,plain,
spl122_298,
inference(avatar_split_clause,[],[f267,f1987]) ).
fof(f1992,definition,
( spl122_299
<=> n7 = sum(n14,n9) ),
introduced(definition,[new_symbols(definition,[spl122_299])],[avatar_definition]) ).
fof(f1995,plain,
spl122_299,
inference(avatar_split_clause,[],[f268,f1992]) ).
fof(f1997,definition,
( spl122_300
<=> n6 = sum(n14,n8) ),
introduced(definition,[new_symbols(definition,[spl122_300])],[avatar_definition]) ).
fof(f2000,plain,
spl122_300,
inference(avatar_split_clause,[],[f269,f1997]) ).
fof(f2002,definition,
( spl122_301
<=> n5 = sum(n14,n7) ),
introduced(definition,[new_symbols(definition,[spl122_301])],[avatar_definition]) ).
fof(f2005,plain,
spl122_301,
inference(avatar_split_clause,[],[f270,f2002]) ).
fof(f2007,definition,
( spl122_302
<=> n4 = sum(n14,n6) ),
introduced(definition,[new_symbols(definition,[spl122_302])],[avatar_definition]) ).
fof(f2010,plain,
spl122_302,
inference(avatar_split_clause,[],[f271,f2007]) ).
fof(f2012,definition,
( spl122_303
<=> n3 = sum(n14,n5) ),
introduced(definition,[new_symbols(definition,[spl122_303])],[avatar_definition]) ).
fof(f2015,plain,
spl122_303,
inference(avatar_split_clause,[],[f272,f2012]) ).
fof(f2017,definition,
( spl122_304
<=> n2 = sum(n14,n4) ),
introduced(definition,[new_symbols(definition,[spl122_304])],[avatar_definition]) ).
fof(f2020,plain,
spl122_304,
inference(avatar_split_clause,[],[f273,f2017]) ).
fof(f2022,definition,
( spl122_305
<=> n1 = sum(n14,n3) ),
introduced(definition,[new_symbols(definition,[spl122_305])],[avatar_definition]) ).
fof(f2025,plain,
spl122_305,
inference(avatar_split_clause,[],[f274,f2022]) ).
fof(f2027,definition,
( spl122_306
<=> n0 = sum(n14,n2) ),
introduced(definition,[new_symbols(definition,[spl122_306])],[avatar_definition]) ).
fof(f2030,plain,
spl122_306,
inference(avatar_split_clause,[],[f275,f2027]) ).
fof(f2032,definition,
( spl122_307
<=> n15 = sum(n14,n1) ),
introduced(definition,[new_symbols(definition,[spl122_307])],[avatar_definition]) ).
fof(f2035,plain,
spl122_307,
inference(avatar_split_clause,[],[f276,f2032]) ).
fof(f2037,definition,
( spl122_308
<=> n14 = sum(n14,n0) ),
introduced(definition,[new_symbols(definition,[spl122_308])],[avatar_definition]) ).
fof(f2040,plain,
spl122_308,
inference(avatar_split_clause,[],[f277,f2037]) ).
fof(f2042,definition,
( spl122_309
<=> n12 = sum(n13,n15) ),
introduced(definition,[new_symbols(definition,[spl122_309])],[avatar_definition]) ).
fof(f2045,plain,
spl122_309,
inference(avatar_split_clause,[],[f278,f2042]) ).
fof(f2047,definition,
( spl122_310
<=> n11 = sum(n13,n14) ),
introduced(definition,[new_symbols(definition,[spl122_310])],[avatar_definition]) ).
fof(f2050,plain,
spl122_310,
inference(avatar_split_clause,[],[f279,f2047]) ).
fof(f2052,definition,
( spl122_311
<=> n10 = sum(n13,n13) ),
introduced(definition,[new_symbols(definition,[spl122_311])],[avatar_definition]) ).
fof(f2055,plain,
spl122_311,
inference(avatar_split_clause,[],[f280,f2052]) ).
fof(f2057,definition,
( spl122_312
<=> n9 = sum(n13,n12) ),
introduced(definition,[new_symbols(definition,[spl122_312])],[avatar_definition]) ).
fof(f2060,plain,
spl122_312,
inference(avatar_split_clause,[],[f281,f2057]) ).
fof(f2062,definition,
( spl122_313
<=> n8 = sum(n13,n11) ),
introduced(definition,[new_symbols(definition,[spl122_313])],[avatar_definition]) ).
fof(f2065,plain,
spl122_313,
inference(avatar_split_clause,[],[f282,f2062]) ).
fof(f2067,definition,
( spl122_314
<=> n7 = sum(n13,n10) ),
introduced(definition,[new_symbols(definition,[spl122_314])],[avatar_definition]) ).
fof(f2070,plain,
spl122_314,
inference(avatar_split_clause,[],[f283,f2067]) ).
fof(f2072,definition,
( spl122_315
<=> n6 = sum(n13,n9) ),
introduced(definition,[new_symbols(definition,[spl122_315])],[avatar_definition]) ).
fof(f2075,plain,
spl122_315,
inference(avatar_split_clause,[],[f284,f2072]) ).
fof(f2077,definition,
( spl122_316
<=> n5 = sum(n13,n8) ),
introduced(definition,[new_symbols(definition,[spl122_316])],[avatar_definition]) ).
fof(f2080,plain,
spl122_316,
inference(avatar_split_clause,[],[f285,f2077]) ).
fof(f2082,definition,
( spl122_317
<=> n4 = sum(n13,n7) ),
introduced(definition,[new_symbols(definition,[spl122_317])],[avatar_definition]) ).
fof(f2085,plain,
spl122_317,
inference(avatar_split_clause,[],[f286,f2082]) ).
fof(f2087,definition,
( spl122_318
<=> n3 = sum(n13,n6) ),
introduced(definition,[new_symbols(definition,[spl122_318])],[avatar_definition]) ).
fof(f2090,plain,
spl122_318,
inference(avatar_split_clause,[],[f287,f2087]) ).
fof(f2092,definition,
( spl122_319
<=> n2 = sum(n13,n5) ),
introduced(definition,[new_symbols(definition,[spl122_319])],[avatar_definition]) ).
fof(f2095,plain,
spl122_319,
inference(avatar_split_clause,[],[f288,f2092]) ).
fof(f2097,definition,
( spl122_320
<=> n1 = sum(n13,n4) ),
introduced(definition,[new_symbols(definition,[spl122_320])],[avatar_definition]) ).
fof(f2100,plain,
spl122_320,
inference(avatar_split_clause,[],[f289,f2097]) ).
fof(f2102,definition,
( spl122_321
<=> n0 = sum(n13,n3) ),
introduced(definition,[new_symbols(definition,[spl122_321])],[avatar_definition]) ).
fof(f2105,plain,
spl122_321,
inference(avatar_split_clause,[],[f290,f2102]) ).
fof(f2107,definition,
( spl122_322
<=> n15 = sum(n13,n2) ),
introduced(definition,[new_symbols(definition,[spl122_322])],[avatar_definition]) ).
fof(f2110,plain,
spl122_322,
inference(avatar_split_clause,[],[f291,f2107]) ).
fof(f2112,definition,
( spl122_323
<=> n14 = sum(n13,n1) ),
introduced(definition,[new_symbols(definition,[spl122_323])],[avatar_definition]) ).
fof(f2115,plain,
spl122_323,
inference(avatar_split_clause,[],[f292,f2112]) ).
fof(f2117,definition,
( spl122_324
<=> n13 = sum(n13,n0) ),
introduced(definition,[new_symbols(definition,[spl122_324])],[avatar_definition]) ).
fof(f2120,plain,
spl122_324,
inference(avatar_split_clause,[],[f293,f2117]) ).
fof(f2122,definition,
( spl122_325
<=> n11 = sum(n12,n15) ),
introduced(definition,[new_symbols(definition,[spl122_325])],[avatar_definition]) ).
fof(f2125,plain,
spl122_325,
inference(avatar_split_clause,[],[f294,f2122]) ).
fof(f2127,definition,
( spl122_326
<=> n10 = sum(n12,n14) ),
introduced(definition,[new_symbols(definition,[spl122_326])],[avatar_definition]) ).
fof(f2130,plain,
spl122_326,
inference(avatar_split_clause,[],[f295,f2127]) ).
fof(f2132,definition,
( spl122_327
<=> n9 = sum(n12,n13) ),
introduced(definition,[new_symbols(definition,[spl122_327])],[avatar_definition]) ).
fof(f2135,plain,
spl122_327,
inference(avatar_split_clause,[],[f296,f2132]) ).
fof(f2137,definition,
( spl122_328
<=> n8 = sum(n12,n12) ),
introduced(definition,[new_symbols(definition,[spl122_328])],[avatar_definition]) ).
fof(f2140,plain,
spl122_328,
inference(avatar_split_clause,[],[f297,f2137]) ).
fof(f2142,definition,
( spl122_329
<=> n7 = sum(n12,n11) ),
introduced(definition,[new_symbols(definition,[spl122_329])],[avatar_definition]) ).
fof(f2145,plain,
spl122_329,
inference(avatar_split_clause,[],[f298,f2142]) ).
fof(f2147,definition,
( spl122_330
<=> n6 = sum(n12,n10) ),
introduced(definition,[new_symbols(definition,[spl122_330])],[avatar_definition]) ).
fof(f2150,plain,
spl122_330,
inference(avatar_split_clause,[],[f299,f2147]) ).
fof(f2152,definition,
( spl122_331
<=> n5 = sum(n12,n9) ),
introduced(definition,[new_symbols(definition,[spl122_331])],[avatar_definition]) ).
fof(f2155,plain,
spl122_331,
inference(avatar_split_clause,[],[f300,f2152]) ).
fof(f2157,definition,
( spl122_332
<=> n4 = sum(n12,n8) ),
introduced(definition,[new_symbols(definition,[spl122_332])],[avatar_definition]) ).
fof(f2160,plain,
spl122_332,
inference(avatar_split_clause,[],[f301,f2157]) ).
fof(f2162,definition,
( spl122_333
<=> n3 = sum(n12,n7) ),
introduced(definition,[new_symbols(definition,[spl122_333])],[avatar_definition]) ).
fof(f2165,plain,
spl122_333,
inference(avatar_split_clause,[],[f302,f2162]) ).
fof(f2167,definition,
( spl122_334
<=> n2 = sum(n12,n6) ),
introduced(definition,[new_symbols(definition,[spl122_334])],[avatar_definition]) ).
fof(f2170,plain,
spl122_334,
inference(avatar_split_clause,[],[f303,f2167]) ).
fof(f2172,definition,
( spl122_335
<=> n1 = sum(n12,n5) ),
introduced(definition,[new_symbols(definition,[spl122_335])],[avatar_definition]) ).
fof(f2175,plain,
spl122_335,
inference(avatar_split_clause,[],[f304,f2172]) ).
fof(f2177,definition,
( spl122_336
<=> n0 = sum(n12,n4) ),
introduced(definition,[new_symbols(definition,[spl122_336])],[avatar_definition]) ).
fof(f2180,plain,
spl122_336,
inference(avatar_split_clause,[],[f305,f2177]) ).
fof(f2182,definition,
( spl122_337
<=> n15 = sum(n12,n3) ),
introduced(definition,[new_symbols(definition,[spl122_337])],[avatar_definition]) ).
fof(f2185,plain,
spl122_337,
inference(avatar_split_clause,[],[f306,f2182]) ).
fof(f2187,definition,
( spl122_338
<=> n14 = sum(n12,n2) ),
introduced(definition,[new_symbols(definition,[spl122_338])],[avatar_definition]) ).
fof(f2190,plain,
spl122_338,
inference(avatar_split_clause,[],[f307,f2187]) ).
fof(f2192,definition,
( spl122_339
<=> n13 = sum(n12,n1) ),
introduced(definition,[new_symbols(definition,[spl122_339])],[avatar_definition]) ).
fof(f2195,plain,
spl122_339,
inference(avatar_split_clause,[],[f308,f2192]) ).
fof(f2197,definition,
( spl122_340
<=> n12 = sum(n12,n0) ),
introduced(definition,[new_symbols(definition,[spl122_340])],[avatar_definition]) ).
fof(f2200,plain,
spl122_340,
inference(avatar_split_clause,[],[f309,f2197]) ).
fof(f2202,definition,
( spl122_341
<=> n10 = sum(n11,n15) ),
introduced(definition,[new_symbols(definition,[spl122_341])],[avatar_definition]) ).
fof(f2205,plain,
spl122_341,
inference(avatar_split_clause,[],[f310,f2202]) ).
fof(f2207,definition,
( spl122_342
<=> n9 = sum(n11,n14) ),
introduced(definition,[new_symbols(definition,[spl122_342])],[avatar_definition]) ).
fof(f2210,plain,
spl122_342,
inference(avatar_split_clause,[],[f311,f2207]) ).
fof(f2212,definition,
( spl122_343
<=> n8 = sum(n11,n13) ),
introduced(definition,[new_symbols(definition,[spl122_343])],[avatar_definition]) ).
fof(f2215,plain,
spl122_343,
inference(avatar_split_clause,[],[f312,f2212]) ).
fof(f2217,definition,
( spl122_344
<=> n7 = sum(n11,n12) ),
introduced(definition,[new_symbols(definition,[spl122_344])],[avatar_definition]) ).
fof(f2220,plain,
spl122_344,
inference(avatar_split_clause,[],[f313,f2217]) ).
fof(f2222,definition,
( spl122_345
<=> n6 = sum(n11,n11) ),
introduced(definition,[new_symbols(definition,[spl122_345])],[avatar_definition]) ).
fof(f2225,plain,
spl122_345,
inference(avatar_split_clause,[],[f314,f2222]) ).
fof(f2227,definition,
( spl122_346
<=> n5 = sum(n11,n10) ),
introduced(definition,[new_symbols(definition,[spl122_346])],[avatar_definition]) ).
fof(f2230,plain,
spl122_346,
inference(avatar_split_clause,[],[f315,f2227]) ).
fof(f2232,definition,
( spl122_347
<=> n4 = sum(n11,n9) ),
introduced(definition,[new_symbols(definition,[spl122_347])],[avatar_definition]) ).
fof(f2235,plain,
spl122_347,
inference(avatar_split_clause,[],[f316,f2232]) ).
fof(f2237,definition,
( spl122_348
<=> n3 = sum(n11,n8) ),
introduced(definition,[new_symbols(definition,[spl122_348])],[avatar_definition]) ).
fof(f2240,plain,
spl122_348,
inference(avatar_split_clause,[],[f317,f2237]) ).
fof(f2242,definition,
( spl122_349
<=> n2 = sum(n11,n7) ),
introduced(definition,[new_symbols(definition,[spl122_349])],[avatar_definition]) ).
fof(f2245,plain,
spl122_349,
inference(avatar_split_clause,[],[f318,f2242]) ).
fof(f2247,definition,
( spl122_350
<=> n1 = sum(n11,n6) ),
introduced(definition,[new_symbols(definition,[spl122_350])],[avatar_definition]) ).
fof(f2250,plain,
spl122_350,
inference(avatar_split_clause,[],[f319,f2247]) ).
fof(f2252,definition,
( spl122_351
<=> n0 = sum(n11,n5) ),
introduced(definition,[new_symbols(definition,[spl122_351])],[avatar_definition]) ).
fof(f2255,plain,
spl122_351,
inference(avatar_split_clause,[],[f320,f2252]) ).
fof(f2257,definition,
( spl122_352
<=> n15 = sum(n11,n4) ),
introduced(definition,[new_symbols(definition,[spl122_352])],[avatar_definition]) ).
fof(f2260,plain,
spl122_352,
inference(avatar_split_clause,[],[f321,f2257]) ).
fof(f2262,definition,
( spl122_353
<=> n14 = sum(n11,n3) ),
introduced(definition,[new_symbols(definition,[spl122_353])],[avatar_definition]) ).
fof(f2265,plain,
spl122_353,
inference(avatar_split_clause,[],[f322,f2262]) ).
fof(f2267,definition,
( spl122_354
<=> n13 = sum(n11,n2) ),
introduced(definition,[new_symbols(definition,[spl122_354])],[avatar_definition]) ).
fof(f2270,plain,
spl122_354,
inference(avatar_split_clause,[],[f323,f2267]) ).
fof(f2272,definition,
( spl122_355
<=> n12 = sum(n11,n1) ),
introduced(definition,[new_symbols(definition,[spl122_355])],[avatar_definition]) ).
fof(f2275,plain,
spl122_355,
inference(avatar_split_clause,[],[f324,f2272]) ).
fof(f2277,definition,
( spl122_356
<=> n11 = sum(n11,n0) ),
introduced(definition,[new_symbols(definition,[spl122_356])],[avatar_definition]) ).
fof(f2280,plain,
spl122_356,
inference(avatar_split_clause,[],[f325,f2277]) ).
fof(f2282,definition,
( spl122_357
<=> n9 = sum(n10,n15) ),
introduced(definition,[new_symbols(definition,[spl122_357])],[avatar_definition]) ).
fof(f2285,plain,
spl122_357,
inference(avatar_split_clause,[],[f326,f2282]) ).
fof(f2287,definition,
( spl122_358
<=> n8 = sum(n10,n14) ),
introduced(definition,[new_symbols(definition,[spl122_358])],[avatar_definition]) ).
fof(f2290,plain,
spl122_358,
inference(avatar_split_clause,[],[f327,f2287]) ).
fof(f2292,definition,
( spl122_359
<=> n7 = sum(n10,n13) ),
introduced(definition,[new_symbols(definition,[spl122_359])],[avatar_definition]) ).
fof(f2295,plain,
spl122_359,
inference(avatar_split_clause,[],[f328,f2292]) ).
fof(f2297,definition,
( spl122_360
<=> n6 = sum(n10,n12) ),
introduced(definition,[new_symbols(definition,[spl122_360])],[avatar_definition]) ).
fof(f2300,plain,
spl122_360,
inference(avatar_split_clause,[],[f329,f2297]) ).
fof(f2302,definition,
( spl122_361
<=> n5 = sum(n10,n11) ),
introduced(definition,[new_symbols(definition,[spl122_361])],[avatar_definition]) ).
fof(f2305,plain,
spl122_361,
inference(avatar_split_clause,[],[f330,f2302]) ).
fof(f2307,definition,
( spl122_362
<=> n4 = sum(n10,n10) ),
introduced(definition,[new_symbols(definition,[spl122_362])],[avatar_definition]) ).
fof(f2310,plain,
spl122_362,
inference(avatar_split_clause,[],[f331,f2307]) ).
fof(f2312,definition,
( spl122_363
<=> n3 = sum(n10,n9) ),
introduced(definition,[new_symbols(definition,[spl122_363])],[avatar_definition]) ).
fof(f2315,plain,
spl122_363,
inference(avatar_split_clause,[],[f332,f2312]) ).
fof(f2317,definition,
( spl122_364
<=> n2 = sum(n10,n8) ),
introduced(definition,[new_symbols(definition,[spl122_364])],[avatar_definition]) ).
fof(f2320,plain,
spl122_364,
inference(avatar_split_clause,[],[f333,f2317]) ).
fof(f2322,definition,
( spl122_365
<=> n1 = sum(n10,n7) ),
introduced(definition,[new_symbols(definition,[spl122_365])],[avatar_definition]) ).
fof(f2325,plain,
spl122_365,
inference(avatar_split_clause,[],[f334,f2322]) ).
fof(f2327,definition,
( spl122_366
<=> n0 = sum(n10,n6) ),
introduced(definition,[new_symbols(definition,[spl122_366])],[avatar_definition]) ).
fof(f2330,plain,
spl122_366,
inference(avatar_split_clause,[],[f335,f2327]) ).
fof(f2332,definition,
( spl122_367
<=> n15 = sum(n10,n5) ),
introduced(definition,[new_symbols(definition,[spl122_367])],[avatar_definition]) ).
fof(f2335,plain,
spl122_367,
inference(avatar_split_clause,[],[f336,f2332]) ).
fof(f2337,definition,
( spl122_368
<=> n14 = sum(n10,n4) ),
introduced(definition,[new_symbols(definition,[spl122_368])],[avatar_definition]) ).
fof(f2340,plain,
spl122_368,
inference(avatar_split_clause,[],[f337,f2337]) ).
fof(f2342,definition,
( spl122_369
<=> n13 = sum(n10,n3) ),
introduced(definition,[new_symbols(definition,[spl122_369])],[avatar_definition]) ).
fof(f2345,plain,
spl122_369,
inference(avatar_split_clause,[],[f338,f2342]) ).
fof(f2347,definition,
( spl122_370
<=> n12 = sum(n10,n2) ),
introduced(definition,[new_symbols(definition,[spl122_370])],[avatar_definition]) ).
fof(f2350,plain,
spl122_370,
inference(avatar_split_clause,[],[f339,f2347]) ).
fof(f2352,definition,
( spl122_371
<=> n11 = sum(n10,n1) ),
introduced(definition,[new_symbols(definition,[spl122_371])],[avatar_definition]) ).
fof(f2355,plain,
spl122_371,
inference(avatar_split_clause,[],[f340,f2352]) ).
fof(f2357,definition,
( spl122_372
<=> n10 = sum(n10,n0) ),
introduced(definition,[new_symbols(definition,[spl122_372])],[avatar_definition]) ).
fof(f2360,plain,
spl122_372,
inference(avatar_split_clause,[],[f341,f2357]) ).
fof(f2362,definition,
( spl122_373
<=> n8 = sum(n9,n15) ),
introduced(definition,[new_symbols(definition,[spl122_373])],[avatar_definition]) ).
fof(f2365,plain,
spl122_373,
inference(avatar_split_clause,[],[f342,f2362]) ).
fof(f2367,definition,
( spl122_374
<=> n7 = sum(n9,n14) ),
introduced(definition,[new_symbols(definition,[spl122_374])],[avatar_definition]) ).
fof(f2370,plain,
spl122_374,
inference(avatar_split_clause,[],[f343,f2367]) ).
fof(f2372,definition,
( spl122_375
<=> n6 = sum(n9,n13) ),
introduced(definition,[new_symbols(definition,[spl122_375])],[avatar_definition]) ).
fof(f2375,plain,
spl122_375,
inference(avatar_split_clause,[],[f344,f2372]) ).
fof(f2377,definition,
( spl122_376
<=> n5 = sum(n9,n12) ),
introduced(definition,[new_symbols(definition,[spl122_376])],[avatar_definition]) ).
fof(f2380,plain,
spl122_376,
inference(avatar_split_clause,[],[f345,f2377]) ).
fof(f2382,definition,
( spl122_377
<=> n4 = sum(n9,n11) ),
introduced(definition,[new_symbols(definition,[spl122_377])],[avatar_definition]) ).
fof(f2385,plain,
spl122_377,
inference(avatar_split_clause,[],[f346,f2382]) ).
fof(f2387,definition,
( spl122_378
<=> n3 = sum(n9,n10) ),
introduced(definition,[new_symbols(definition,[spl122_378])],[avatar_definition]) ).
fof(f2390,plain,
spl122_378,
inference(avatar_split_clause,[],[f347,f2387]) ).
fof(f2392,definition,
( spl122_379
<=> n2 = sum(n9,n9) ),
introduced(definition,[new_symbols(definition,[spl122_379])],[avatar_definition]) ).
fof(f2395,plain,
spl122_379,
inference(avatar_split_clause,[],[f348,f2392]) ).
fof(f2397,definition,
( spl122_380
<=> n1 = sum(n9,n8) ),
introduced(definition,[new_symbols(definition,[spl122_380])],[avatar_definition]) ).
fof(f2400,plain,
spl122_380,
inference(avatar_split_clause,[],[f349,f2397]) ).
fof(f2402,definition,
( spl122_381
<=> n0 = sum(n9,n7) ),
introduced(definition,[new_symbols(definition,[spl122_381])],[avatar_definition]) ).
fof(f2405,plain,
spl122_381,
inference(avatar_split_clause,[],[f350,f2402]) ).
fof(f2407,definition,
( spl122_382
<=> n15 = sum(n9,n6) ),
introduced(definition,[new_symbols(definition,[spl122_382])],[avatar_definition]) ).
fof(f2410,plain,
spl122_382,
inference(avatar_split_clause,[],[f351,f2407]) ).
fof(f2412,definition,
( spl122_383
<=> n14 = sum(n9,n5) ),
introduced(definition,[new_symbols(definition,[spl122_383])],[avatar_definition]) ).
fof(f2415,plain,
spl122_383,
inference(avatar_split_clause,[],[f352,f2412]) ).
fof(f2417,definition,
( spl122_384
<=> n13 = sum(n9,n4) ),
introduced(definition,[new_symbols(definition,[spl122_384])],[avatar_definition]) ).
fof(f2420,plain,
spl122_384,
inference(avatar_split_clause,[],[f353,f2417]) ).
fof(f2422,definition,
( spl122_385
<=> n12 = sum(n9,n3) ),
introduced(definition,[new_symbols(definition,[spl122_385])],[avatar_definition]) ).
fof(f2425,plain,
spl122_385,
inference(avatar_split_clause,[],[f354,f2422]) ).
fof(f2427,definition,
( spl122_386
<=> n11 = sum(n9,n2) ),
introduced(definition,[new_symbols(definition,[spl122_386])],[avatar_definition]) ).
fof(f2430,plain,
spl122_386,
inference(avatar_split_clause,[],[f355,f2427]) ).
fof(f2432,definition,
( spl122_387
<=> n10 = sum(n9,n1) ),
introduced(definition,[new_symbols(definition,[spl122_387])],[avatar_definition]) ).
fof(f2435,plain,
spl122_387,
inference(avatar_split_clause,[],[f356,f2432]) ).
fof(f2437,definition,
( spl122_388
<=> n9 = sum(n9,n0) ),
introduced(definition,[new_symbols(definition,[spl122_388])],[avatar_definition]) ).
fof(f2440,plain,
spl122_388,
inference(avatar_split_clause,[],[f357,f2437]) ).
fof(f2442,definition,
( spl122_389
<=> n7 = sum(n8,n15) ),
introduced(definition,[new_symbols(definition,[spl122_389])],[avatar_definition]) ).
fof(f2445,plain,
spl122_389,
inference(avatar_split_clause,[],[f358,f2442]) ).
fof(f2447,definition,
( spl122_390
<=> n6 = sum(n8,n14) ),
introduced(definition,[new_symbols(definition,[spl122_390])],[avatar_definition]) ).
fof(f2450,plain,
spl122_390,
inference(avatar_split_clause,[],[f359,f2447]) ).
fof(f2452,definition,
( spl122_391
<=> n5 = sum(n8,n13) ),
introduced(definition,[new_symbols(definition,[spl122_391])],[avatar_definition]) ).
fof(f2455,plain,
spl122_391,
inference(avatar_split_clause,[],[f360,f2452]) ).
fof(f2457,definition,
( spl122_392
<=> n4 = sum(n8,n12) ),
introduced(definition,[new_symbols(definition,[spl122_392])],[avatar_definition]) ).
fof(f2460,plain,
spl122_392,
inference(avatar_split_clause,[],[f361,f2457]) ).
fof(f2462,definition,
( spl122_393
<=> n3 = sum(n8,n11) ),
introduced(definition,[new_symbols(definition,[spl122_393])],[avatar_definition]) ).
fof(f2465,plain,
spl122_393,
inference(avatar_split_clause,[],[f362,f2462]) ).
fof(f2467,definition,
( spl122_394
<=> n2 = sum(n8,n10) ),
introduced(definition,[new_symbols(definition,[spl122_394])],[avatar_definition]) ).
fof(f2470,plain,
spl122_394,
inference(avatar_split_clause,[],[f363,f2467]) ).
fof(f2472,definition,
( spl122_395
<=> n1 = sum(n8,n9) ),
introduced(definition,[new_symbols(definition,[spl122_395])],[avatar_definition]) ).
fof(f2475,plain,
spl122_395,
inference(avatar_split_clause,[],[f364,f2472]) ).
fof(f2477,definition,
( spl122_396
<=> n0 = sum(n8,n8) ),
introduced(definition,[new_symbols(definition,[spl122_396])],[avatar_definition]) ).
fof(f2480,plain,
spl122_396,
inference(avatar_split_clause,[],[f365,f2477]) ).
fof(f2482,definition,
( spl122_397
<=> n15 = sum(n8,n7) ),
introduced(definition,[new_symbols(definition,[spl122_397])],[avatar_definition]) ).
fof(f2485,plain,
spl122_397,
inference(avatar_split_clause,[],[f366,f2482]) ).
fof(f2487,definition,
( spl122_398
<=> n14 = sum(n8,n6) ),
introduced(definition,[new_symbols(definition,[spl122_398])],[avatar_definition]) ).
fof(f2490,plain,
spl122_398,
inference(avatar_split_clause,[],[f367,f2487]) ).
fof(f2492,definition,
( spl122_399
<=> n13 = sum(n8,n5) ),
introduced(definition,[new_symbols(definition,[spl122_399])],[avatar_definition]) ).
fof(f2495,plain,
spl122_399,
inference(avatar_split_clause,[],[f368,f2492]) ).
fof(f2497,definition,
( spl122_400
<=> n12 = sum(n8,n4) ),
introduced(definition,[new_symbols(definition,[spl122_400])],[avatar_definition]) ).
fof(f2500,plain,
spl122_400,
inference(avatar_split_clause,[],[f369,f2497]) ).
fof(f2502,definition,
( spl122_401
<=> n11 = sum(n8,n3) ),
introduced(definition,[new_symbols(definition,[spl122_401])],[avatar_definition]) ).
fof(f2505,plain,
spl122_401,
inference(avatar_split_clause,[],[f370,f2502]) ).
fof(f2507,definition,
( spl122_402
<=> n10 = sum(n8,n2) ),
introduced(definition,[new_symbols(definition,[spl122_402])],[avatar_definition]) ).
fof(f2510,plain,
spl122_402,
inference(avatar_split_clause,[],[f371,f2507]) ).
fof(f2512,definition,
( spl122_403
<=> n9 = sum(n8,n1) ),
introduced(definition,[new_symbols(definition,[spl122_403])],[avatar_definition]) ).
fof(f2515,plain,
spl122_403,
inference(avatar_split_clause,[],[f372,f2512]) ).
fof(f2517,definition,
( spl122_404
<=> n8 = sum(n8,n0) ),
introduced(definition,[new_symbols(definition,[spl122_404])],[avatar_definition]) ).
fof(f2520,plain,
spl122_404,
inference(avatar_split_clause,[],[f373,f2517]) ).
fof(f2522,definition,
( spl122_405
<=> n6 = sum(n7,n15) ),
introduced(definition,[new_symbols(definition,[spl122_405])],[avatar_definition]) ).
fof(f2525,plain,
spl122_405,
inference(avatar_split_clause,[],[f374,f2522]) ).
fof(f2527,definition,
( spl122_406
<=> n5 = sum(n7,n14) ),
introduced(definition,[new_symbols(definition,[spl122_406])],[avatar_definition]) ).
fof(f2530,plain,
spl122_406,
inference(avatar_split_clause,[],[f375,f2527]) ).
fof(f2532,definition,
( spl122_407
<=> n4 = sum(n7,n13) ),
introduced(definition,[new_symbols(definition,[spl122_407])],[avatar_definition]) ).
fof(f2535,plain,
spl122_407,
inference(avatar_split_clause,[],[f376,f2532]) ).
fof(f2537,definition,
( spl122_408
<=> n3 = sum(n7,n12) ),
introduced(definition,[new_symbols(definition,[spl122_408])],[avatar_definition]) ).
fof(f2540,plain,
spl122_408,
inference(avatar_split_clause,[],[f377,f2537]) ).
fof(f2542,definition,
( spl122_409
<=> n2 = sum(n7,n11) ),
introduced(definition,[new_symbols(definition,[spl122_409])],[avatar_definition]) ).
fof(f2545,plain,
spl122_409,
inference(avatar_split_clause,[],[f378,f2542]) ).
fof(f2547,definition,
( spl122_410
<=> n1 = sum(n7,n10) ),
introduced(definition,[new_symbols(definition,[spl122_410])],[avatar_definition]) ).
fof(f2550,plain,
spl122_410,
inference(avatar_split_clause,[],[f379,f2547]) ).
fof(f2552,definition,
( spl122_411
<=> n0 = sum(n7,n9) ),
introduced(definition,[new_symbols(definition,[spl122_411])],[avatar_definition]) ).
fof(f2555,plain,
spl122_411,
inference(avatar_split_clause,[],[f380,f2552]) ).
fof(f2557,definition,
( spl122_412
<=> n15 = sum(n7,n8) ),
introduced(definition,[new_symbols(definition,[spl122_412])],[avatar_definition]) ).
fof(f2560,plain,
spl122_412,
inference(avatar_split_clause,[],[f381,f2557]) ).
fof(f2562,definition,
( spl122_413
<=> n14 = sum(n7,n7) ),
introduced(definition,[new_symbols(definition,[spl122_413])],[avatar_definition]) ).
fof(f2565,plain,
spl122_413,
inference(avatar_split_clause,[],[f382,f2562]) ).
fof(f2567,definition,
( spl122_414
<=> n13 = sum(n7,n6) ),
introduced(definition,[new_symbols(definition,[spl122_414])],[avatar_definition]) ).
fof(f2570,plain,
spl122_414,
inference(avatar_split_clause,[],[f383,f2567]) ).
fof(f2572,definition,
( spl122_415
<=> n12 = sum(n7,n5) ),
introduced(definition,[new_symbols(definition,[spl122_415])],[avatar_definition]) ).
fof(f2575,plain,
spl122_415,
inference(avatar_split_clause,[],[f384,f2572]) ).
fof(f2577,definition,
( spl122_416
<=> n11 = sum(n7,n4) ),
introduced(definition,[new_symbols(definition,[spl122_416])],[avatar_definition]) ).
fof(f2580,plain,
spl122_416,
inference(avatar_split_clause,[],[f385,f2577]) ).
fof(f2582,definition,
( spl122_417
<=> n10 = sum(n7,n3) ),
introduced(definition,[new_symbols(definition,[spl122_417])],[avatar_definition]) ).
fof(f2585,plain,
spl122_417,
inference(avatar_split_clause,[],[f386,f2582]) ).
fof(f2587,definition,
( spl122_418
<=> n9 = sum(n7,n2) ),
introduced(definition,[new_symbols(definition,[spl122_418])],[avatar_definition]) ).
fof(f2590,plain,
spl122_418,
inference(avatar_split_clause,[],[f387,f2587]) ).
fof(f2592,definition,
( spl122_419
<=> n8 = sum(n7,n1) ),
introduced(definition,[new_symbols(definition,[spl122_419])],[avatar_definition]) ).
fof(f2595,plain,
spl122_419,
inference(avatar_split_clause,[],[f388,f2592]) ).
fof(f2597,definition,
( spl122_420
<=> n7 = sum(n7,n0) ),
introduced(definition,[new_symbols(definition,[spl122_420])],[avatar_definition]) ).
fof(f2600,plain,
spl122_420,
inference(avatar_split_clause,[],[f389,f2597]) ).
fof(f2602,definition,
( spl122_421
<=> n5 = sum(n6,n15) ),
introduced(definition,[new_symbols(definition,[spl122_421])],[avatar_definition]) ).
fof(f2605,plain,
spl122_421,
inference(avatar_split_clause,[],[f390,f2602]) ).
fof(f2607,definition,
( spl122_422
<=> n4 = sum(n6,n14) ),
introduced(definition,[new_symbols(definition,[spl122_422])],[avatar_definition]) ).
fof(f2610,plain,
spl122_422,
inference(avatar_split_clause,[],[f391,f2607]) ).
fof(f2612,definition,
( spl122_423
<=> n3 = sum(n6,n13) ),
introduced(definition,[new_symbols(definition,[spl122_423])],[avatar_definition]) ).
fof(f2615,plain,
spl122_423,
inference(avatar_split_clause,[],[f392,f2612]) ).
fof(f2617,definition,
( spl122_424
<=> n2 = sum(n6,n12) ),
introduced(definition,[new_symbols(definition,[spl122_424])],[avatar_definition]) ).
fof(f2620,plain,
spl122_424,
inference(avatar_split_clause,[],[f393,f2617]) ).
fof(f2622,definition,
( spl122_425
<=> n1 = sum(n6,n11) ),
introduced(definition,[new_symbols(definition,[spl122_425])],[avatar_definition]) ).
fof(f2625,plain,
spl122_425,
inference(avatar_split_clause,[],[f394,f2622]) ).
fof(f2627,definition,
( spl122_426
<=> n0 = sum(n6,n10) ),
introduced(definition,[new_symbols(definition,[spl122_426])],[avatar_definition]) ).
fof(f2630,plain,
spl122_426,
inference(avatar_split_clause,[],[f395,f2627]) ).
fof(f2632,definition,
( spl122_427
<=> n15 = sum(n6,n9) ),
introduced(definition,[new_symbols(definition,[spl122_427])],[avatar_definition]) ).
fof(f2635,plain,
spl122_427,
inference(avatar_split_clause,[],[f396,f2632]) ).
fof(f2637,definition,
( spl122_428
<=> n14 = sum(n6,n8) ),
introduced(definition,[new_symbols(definition,[spl122_428])],[avatar_definition]) ).
fof(f2640,plain,
spl122_428,
inference(avatar_split_clause,[],[f397,f2637]) ).
fof(f2642,definition,
( spl122_429
<=> n13 = sum(n6,n7) ),
introduced(definition,[new_symbols(definition,[spl122_429])],[avatar_definition]) ).
fof(f2645,plain,
spl122_429,
inference(avatar_split_clause,[],[f398,f2642]) ).
fof(f2647,definition,
( spl122_430
<=> n12 = sum(n6,n6) ),
introduced(definition,[new_symbols(definition,[spl122_430])],[avatar_definition]) ).
fof(f2650,plain,
spl122_430,
inference(avatar_split_clause,[],[f399,f2647]) ).
fof(f2652,definition,
( spl122_431
<=> n11 = sum(n6,n5) ),
introduced(definition,[new_symbols(definition,[spl122_431])],[avatar_definition]) ).
fof(f2655,plain,
spl122_431,
inference(avatar_split_clause,[],[f400,f2652]) ).
fof(f2657,definition,
( spl122_432
<=> n10 = sum(n6,n4) ),
introduced(definition,[new_symbols(definition,[spl122_432])],[avatar_definition]) ).
fof(f2660,plain,
spl122_432,
inference(avatar_split_clause,[],[f401,f2657]) ).
fof(f2662,definition,
( spl122_433
<=> n9 = sum(n6,n3) ),
introduced(definition,[new_symbols(definition,[spl122_433])],[avatar_definition]) ).
fof(f2665,plain,
spl122_433,
inference(avatar_split_clause,[],[f402,f2662]) ).
fof(f2667,definition,
( spl122_434
<=> n8 = sum(n6,n2) ),
introduced(definition,[new_symbols(definition,[spl122_434])],[avatar_definition]) ).
fof(f2670,plain,
spl122_434,
inference(avatar_split_clause,[],[f403,f2667]) ).
fof(f2672,definition,
( spl122_435
<=> n7 = sum(n6,n1) ),
introduced(definition,[new_symbols(definition,[spl122_435])],[avatar_definition]) ).
fof(f2675,plain,
spl122_435,
inference(avatar_split_clause,[],[f404,f2672]) ).
fof(f2677,definition,
( spl122_436
<=> n6 = sum(n6,n0) ),
introduced(definition,[new_symbols(definition,[spl122_436])],[avatar_definition]) ).
fof(f2680,plain,
spl122_436,
inference(avatar_split_clause,[],[f405,f2677]) ).
fof(f2682,definition,
( spl122_437
<=> n4 = sum(n5,n15) ),
introduced(definition,[new_symbols(definition,[spl122_437])],[avatar_definition]) ).
fof(f2685,plain,
spl122_437,
inference(avatar_split_clause,[],[f406,f2682]) ).
fof(f2687,definition,
( spl122_438
<=> n3 = sum(n5,n14) ),
introduced(definition,[new_symbols(definition,[spl122_438])],[avatar_definition]) ).
fof(f2690,plain,
spl122_438,
inference(avatar_split_clause,[],[f407,f2687]) ).
fof(f2692,definition,
( spl122_439
<=> n2 = sum(n5,n13) ),
introduced(definition,[new_symbols(definition,[spl122_439])],[avatar_definition]) ).
fof(f2695,plain,
spl122_439,
inference(avatar_split_clause,[],[f408,f2692]) ).
fof(f2697,definition,
( spl122_440
<=> n1 = sum(n5,n12) ),
introduced(definition,[new_symbols(definition,[spl122_440])],[avatar_definition]) ).
fof(f2700,plain,
spl122_440,
inference(avatar_split_clause,[],[f409,f2697]) ).
fof(f2702,definition,
( spl122_441
<=> n0 = sum(n5,n11) ),
introduced(definition,[new_symbols(definition,[spl122_441])],[avatar_definition]) ).
fof(f2705,plain,
spl122_441,
inference(avatar_split_clause,[],[f410,f2702]) ).
fof(f2707,definition,
( spl122_442
<=> n15 = sum(n5,n10) ),
introduced(definition,[new_symbols(definition,[spl122_442])],[avatar_definition]) ).
fof(f2710,plain,
spl122_442,
inference(avatar_split_clause,[],[f411,f2707]) ).
fof(f2712,definition,
( spl122_443
<=> n14 = sum(n5,n9) ),
introduced(definition,[new_symbols(definition,[spl122_443])],[avatar_definition]) ).
fof(f2715,plain,
spl122_443,
inference(avatar_split_clause,[],[f412,f2712]) ).
fof(f2717,definition,
( spl122_444
<=> n13 = sum(n5,n8) ),
introduced(definition,[new_symbols(definition,[spl122_444])],[avatar_definition]) ).
fof(f2720,plain,
spl122_444,
inference(avatar_split_clause,[],[f413,f2717]) ).
fof(f2722,definition,
( spl122_445
<=> n12 = sum(n5,n7) ),
introduced(definition,[new_symbols(definition,[spl122_445])],[avatar_definition]) ).
fof(f2725,plain,
spl122_445,
inference(avatar_split_clause,[],[f414,f2722]) ).
fof(f2727,definition,
( spl122_446
<=> n11 = sum(n5,n6) ),
introduced(definition,[new_symbols(definition,[spl122_446])],[avatar_definition]) ).
fof(f2730,plain,
spl122_446,
inference(avatar_split_clause,[],[f415,f2727]) ).
fof(f2732,definition,
( spl122_447
<=> n10 = sum(n5,n5) ),
introduced(definition,[new_symbols(definition,[spl122_447])],[avatar_definition]) ).
fof(f2735,plain,
spl122_447,
inference(avatar_split_clause,[],[f416,f2732]) ).
fof(f2737,definition,
( spl122_448
<=> n9 = sum(n5,n4) ),
introduced(definition,[new_symbols(definition,[spl122_448])],[avatar_definition]) ).
fof(f2740,plain,
spl122_448,
inference(avatar_split_clause,[],[f417,f2737]) ).
fof(f2742,definition,
( spl122_449
<=> n8 = sum(n5,n3) ),
introduced(definition,[new_symbols(definition,[spl122_449])],[avatar_definition]) ).
fof(f2745,plain,
spl122_449,
inference(avatar_split_clause,[],[f418,f2742]) ).
fof(f2747,definition,
( spl122_450
<=> n7 = sum(n5,n2) ),
introduced(definition,[new_symbols(definition,[spl122_450])],[avatar_definition]) ).
fof(f2750,plain,
spl122_450,
inference(avatar_split_clause,[],[f419,f2747]) ).
fof(f2752,definition,
( spl122_451
<=> n6 = sum(n5,n1) ),
introduced(definition,[new_symbols(definition,[spl122_451])],[avatar_definition]) ).
fof(f2755,plain,
spl122_451,
inference(avatar_split_clause,[],[f420,f2752]) ).
fof(f2757,definition,
( spl122_452
<=> n5 = sum(n5,n0) ),
introduced(definition,[new_symbols(definition,[spl122_452])],[avatar_definition]) ).
fof(f2760,plain,
spl122_452,
inference(avatar_split_clause,[],[f421,f2757]) ).
fof(f2762,definition,
( spl122_453
<=> n3 = sum(n4,n15) ),
introduced(definition,[new_symbols(definition,[spl122_453])],[avatar_definition]) ).
fof(f2765,plain,
spl122_453,
inference(avatar_split_clause,[],[f422,f2762]) ).
fof(f2767,definition,
( spl122_454
<=> n2 = sum(n4,n14) ),
introduced(definition,[new_symbols(definition,[spl122_454])],[avatar_definition]) ).
fof(f2770,plain,
spl122_454,
inference(avatar_split_clause,[],[f423,f2767]) ).
fof(f2772,definition,
( spl122_455
<=> n1 = sum(n4,n13) ),
introduced(definition,[new_symbols(definition,[spl122_455])],[avatar_definition]) ).
fof(f2775,plain,
spl122_455,
inference(avatar_split_clause,[],[f424,f2772]) ).
fof(f2777,definition,
( spl122_456
<=> n0 = sum(n4,n12) ),
introduced(definition,[new_symbols(definition,[spl122_456])],[avatar_definition]) ).
fof(f2780,plain,
spl122_456,
inference(avatar_split_clause,[],[f425,f2777]) ).
fof(f2782,definition,
( spl122_457
<=> n15 = sum(n4,n11) ),
introduced(definition,[new_symbols(definition,[spl122_457])],[avatar_definition]) ).
fof(f2785,plain,
spl122_457,
inference(avatar_split_clause,[],[f426,f2782]) ).
fof(f2787,definition,
( spl122_458
<=> n14 = sum(n4,n10) ),
introduced(definition,[new_symbols(definition,[spl122_458])],[avatar_definition]) ).
fof(f2790,plain,
spl122_458,
inference(avatar_split_clause,[],[f427,f2787]) ).
fof(f2792,definition,
( spl122_459
<=> n13 = sum(n4,n9) ),
introduced(definition,[new_symbols(definition,[spl122_459])],[avatar_definition]) ).
fof(f2795,plain,
spl122_459,
inference(avatar_split_clause,[],[f428,f2792]) ).
fof(f2797,definition,
( spl122_460
<=> n12 = sum(n4,n8) ),
introduced(definition,[new_symbols(definition,[spl122_460])],[avatar_definition]) ).
fof(f2800,plain,
spl122_460,
inference(avatar_split_clause,[],[f429,f2797]) ).
fof(f2802,definition,
( spl122_461
<=> n11 = sum(n4,n7) ),
introduced(definition,[new_symbols(definition,[spl122_461])],[avatar_definition]) ).
fof(f2805,plain,
spl122_461,
inference(avatar_split_clause,[],[f430,f2802]) ).
fof(f2807,definition,
( spl122_462
<=> n10 = sum(n4,n6) ),
introduced(definition,[new_symbols(definition,[spl122_462])],[avatar_definition]) ).
fof(f2810,plain,
spl122_462,
inference(avatar_split_clause,[],[f431,f2807]) ).
fof(f2812,definition,
( spl122_463
<=> n9 = sum(n4,n5) ),
introduced(definition,[new_symbols(definition,[spl122_463])],[avatar_definition]) ).
fof(f2815,plain,
spl122_463,
inference(avatar_split_clause,[],[f432,f2812]) ).
fof(f2817,definition,
( spl122_464
<=> n8 = sum(n4,n4) ),
introduced(definition,[new_symbols(definition,[spl122_464])],[avatar_definition]) ).
fof(f2820,plain,
spl122_464,
inference(avatar_split_clause,[],[f433,f2817]) ).
fof(f2822,definition,
( spl122_465
<=> n7 = sum(n4,n3) ),
introduced(definition,[new_symbols(definition,[spl122_465])],[avatar_definition]) ).
fof(f2825,plain,
spl122_465,
inference(avatar_split_clause,[],[f434,f2822]) ).
fof(f2827,definition,
( spl122_466
<=> n6 = sum(n4,n2) ),
introduced(definition,[new_symbols(definition,[spl122_466])],[avatar_definition]) ).
fof(f2830,plain,
spl122_466,
inference(avatar_split_clause,[],[f435,f2827]) ).
fof(f2832,definition,
( spl122_467
<=> n5 = sum(n4,n1) ),
introduced(definition,[new_symbols(definition,[spl122_467])],[avatar_definition]) ).
fof(f2835,plain,
spl122_467,
inference(avatar_split_clause,[],[f436,f2832]) ).
fof(f2837,definition,
( spl122_468
<=> n4 = sum(n4,n0) ),
introduced(definition,[new_symbols(definition,[spl122_468])],[avatar_definition]) ).
fof(f2840,plain,
spl122_468,
inference(avatar_split_clause,[],[f437,f2837]) ).
fof(f2842,definition,
( spl122_469
<=> n2 = sum(n3,n15) ),
introduced(definition,[new_symbols(definition,[spl122_469])],[avatar_definition]) ).
fof(f2845,plain,
spl122_469,
inference(avatar_split_clause,[],[f438,f2842]) ).
fof(f2847,definition,
( spl122_470
<=> n1 = sum(n3,n14) ),
introduced(definition,[new_symbols(definition,[spl122_470])],[avatar_definition]) ).
fof(f2850,plain,
spl122_470,
inference(avatar_split_clause,[],[f439,f2847]) ).
fof(f2852,definition,
( spl122_471
<=> n0 = sum(n3,n13) ),
introduced(definition,[new_symbols(definition,[spl122_471])],[avatar_definition]) ).
fof(f2855,plain,
spl122_471,
inference(avatar_split_clause,[],[f440,f2852]) ).
fof(f2857,definition,
( spl122_472
<=> n15 = sum(n3,n12) ),
introduced(definition,[new_symbols(definition,[spl122_472])],[avatar_definition]) ).
fof(f2860,plain,
spl122_472,
inference(avatar_split_clause,[],[f441,f2857]) ).
fof(f2862,definition,
( spl122_473
<=> n14 = sum(n3,n11) ),
introduced(definition,[new_symbols(definition,[spl122_473])],[avatar_definition]) ).
fof(f2865,plain,
spl122_473,
inference(avatar_split_clause,[],[f442,f2862]) ).
fof(f2867,definition,
( spl122_474
<=> n13 = sum(n3,n10) ),
introduced(definition,[new_symbols(definition,[spl122_474])],[avatar_definition]) ).
fof(f2870,plain,
spl122_474,
inference(avatar_split_clause,[],[f443,f2867]) ).
fof(f2872,definition,
( spl122_475
<=> n12 = sum(n3,n9) ),
introduced(definition,[new_symbols(definition,[spl122_475])],[avatar_definition]) ).
fof(f2875,plain,
spl122_475,
inference(avatar_split_clause,[],[f444,f2872]) ).
fof(f2877,definition,
( spl122_476
<=> n11 = sum(n3,n8) ),
introduced(definition,[new_symbols(definition,[spl122_476])],[avatar_definition]) ).
fof(f2880,plain,
spl122_476,
inference(avatar_split_clause,[],[f445,f2877]) ).
fof(f2882,definition,
( spl122_477
<=> n10 = sum(n3,n7) ),
introduced(definition,[new_symbols(definition,[spl122_477])],[avatar_definition]) ).
fof(f2885,plain,
spl122_477,
inference(avatar_split_clause,[],[f446,f2882]) ).
fof(f2887,definition,
( spl122_478
<=> n9 = sum(n3,n6) ),
introduced(definition,[new_symbols(definition,[spl122_478])],[avatar_definition]) ).
fof(f2890,plain,
spl122_478,
inference(avatar_split_clause,[],[f447,f2887]) ).
fof(f2892,definition,
( spl122_479
<=> n8 = sum(n3,n5) ),
introduced(definition,[new_symbols(definition,[spl122_479])],[avatar_definition]) ).
fof(f2895,plain,
spl122_479,
inference(avatar_split_clause,[],[f448,f2892]) ).
fof(f2897,definition,
( spl122_480
<=> n7 = sum(n3,n4) ),
introduced(definition,[new_symbols(definition,[spl122_480])],[avatar_definition]) ).
fof(f2900,plain,
spl122_480,
inference(avatar_split_clause,[],[f449,f2897]) ).
fof(f2902,definition,
( spl122_481
<=> n6 = sum(n3,n3) ),
introduced(definition,[new_symbols(definition,[spl122_481])],[avatar_definition]) ).
fof(f2905,plain,
spl122_481,
inference(avatar_split_clause,[],[f450,f2902]) ).
fof(f2907,definition,
( spl122_482
<=> n5 = sum(n3,n2) ),
introduced(definition,[new_symbols(definition,[spl122_482])],[avatar_definition]) ).
fof(f2910,plain,
spl122_482,
inference(avatar_split_clause,[],[f451,f2907]) ).
fof(f2912,definition,
( spl122_483
<=> n4 = sum(n3,n1) ),
introduced(definition,[new_symbols(definition,[spl122_483])],[avatar_definition]) ).
fof(f2915,plain,
spl122_483,
inference(avatar_split_clause,[],[f452,f2912]) ).
fof(f2917,definition,
( spl122_484
<=> n3 = sum(n3,n0) ),
introduced(definition,[new_symbols(definition,[spl122_484])],[avatar_definition]) ).
fof(f2920,plain,
spl122_484,
inference(avatar_split_clause,[],[f453,f2917]) ).
fof(f2922,definition,
( spl122_485
<=> n1 = sum(n2,n15) ),
introduced(definition,[new_symbols(definition,[spl122_485])],[avatar_definition]) ).
fof(f2925,plain,
spl122_485,
inference(avatar_split_clause,[],[f454,f2922]) ).
fof(f2927,definition,
( spl122_486
<=> n0 = sum(n2,n14) ),
introduced(definition,[new_symbols(definition,[spl122_486])],[avatar_definition]) ).
fof(f2930,plain,
spl122_486,
inference(avatar_split_clause,[],[f455,f2927]) ).
fof(f2932,definition,
( spl122_487
<=> n15 = sum(n2,n13) ),
introduced(definition,[new_symbols(definition,[spl122_487])],[avatar_definition]) ).
fof(f2935,plain,
spl122_487,
inference(avatar_split_clause,[],[f456,f2932]) ).
fof(f2937,definition,
( spl122_488
<=> n14 = sum(n2,n12) ),
introduced(definition,[new_symbols(definition,[spl122_488])],[avatar_definition]) ).
fof(f2940,plain,
spl122_488,
inference(avatar_split_clause,[],[f457,f2937]) ).
fof(f2942,definition,
( spl122_489
<=> n13 = sum(n2,n11) ),
introduced(definition,[new_symbols(definition,[spl122_489])],[avatar_definition]) ).
fof(f2945,plain,
spl122_489,
inference(avatar_split_clause,[],[f458,f2942]) ).
fof(f2947,definition,
( spl122_490
<=> n12 = sum(n2,n10) ),
introduced(definition,[new_symbols(definition,[spl122_490])],[avatar_definition]) ).
fof(f2950,plain,
spl122_490,
inference(avatar_split_clause,[],[f459,f2947]) ).
fof(f2952,definition,
( spl122_491
<=> n11 = sum(n2,n9) ),
introduced(definition,[new_symbols(definition,[spl122_491])],[avatar_definition]) ).
fof(f2955,plain,
spl122_491,
inference(avatar_split_clause,[],[f460,f2952]) ).
fof(f2957,definition,
( spl122_492
<=> n10 = sum(n2,n8) ),
introduced(definition,[new_symbols(definition,[spl122_492])],[avatar_definition]) ).
fof(f2960,plain,
spl122_492,
inference(avatar_split_clause,[],[f461,f2957]) ).
fof(f2962,definition,
( spl122_493
<=> n9 = sum(n2,n7) ),
introduced(definition,[new_symbols(definition,[spl122_493])],[avatar_definition]) ).
fof(f2965,plain,
spl122_493,
inference(avatar_split_clause,[],[f462,f2962]) ).
fof(f2967,definition,
( spl122_494
<=> n8 = sum(n2,n6) ),
introduced(definition,[new_symbols(definition,[spl122_494])],[avatar_definition]) ).
fof(f2970,plain,
spl122_494,
inference(avatar_split_clause,[],[f463,f2967]) ).
fof(f2972,definition,
( spl122_495
<=> n7 = sum(n2,n5) ),
introduced(definition,[new_symbols(definition,[spl122_495])],[avatar_definition]) ).
fof(f2975,plain,
spl122_495,
inference(avatar_split_clause,[],[f464,f2972]) ).
fof(f2977,definition,
( spl122_496
<=> n6 = sum(n2,n4) ),
introduced(definition,[new_symbols(definition,[spl122_496])],[avatar_definition]) ).
fof(f2980,plain,
spl122_496,
inference(avatar_split_clause,[],[f465,f2977]) ).
fof(f2982,definition,
( spl122_497
<=> n5 = sum(n2,n3) ),
introduced(definition,[new_symbols(definition,[spl122_497])],[avatar_definition]) ).
fof(f2985,plain,
spl122_497,
inference(avatar_split_clause,[],[f466,f2982]) ).
fof(f2987,definition,
( spl122_498
<=> n4 = sum(n2,n2) ),
introduced(definition,[new_symbols(definition,[spl122_498])],[avatar_definition]) ).
fof(f2990,plain,
spl122_498,
inference(avatar_split_clause,[],[f467,f2987]) ).
fof(f2992,definition,
( spl122_499
<=> n3 = sum(n2,n1) ),
introduced(definition,[new_symbols(definition,[spl122_499])],[avatar_definition]) ).
fof(f2995,plain,
spl122_499,
inference(avatar_split_clause,[],[f468,f2992]) ).
fof(f2997,definition,
( spl122_500
<=> n2 = sum(n2,n0) ),
introduced(definition,[new_symbols(definition,[spl122_500])],[avatar_definition]) ).
fof(f3000,plain,
spl122_500,
inference(avatar_split_clause,[],[f469,f2997]) ).
fof(f3002,definition,
( spl122_501
<=> n0 = sum(n1,n15) ),
introduced(definition,[new_symbols(definition,[spl122_501])],[avatar_definition]) ).
fof(f3005,plain,
spl122_501,
inference(avatar_split_clause,[],[f470,f3002]) ).
fof(f3007,definition,
( spl122_502
<=> n15 = sum(n1,n14) ),
introduced(definition,[new_symbols(definition,[spl122_502])],[avatar_definition]) ).
fof(f3010,plain,
spl122_502,
inference(avatar_split_clause,[],[f471,f3007]) ).
fof(f3012,definition,
( spl122_503
<=> n14 = sum(n1,n13) ),
introduced(definition,[new_symbols(definition,[spl122_503])],[avatar_definition]) ).
fof(f3015,plain,
spl122_503,
inference(avatar_split_clause,[],[f472,f3012]) ).
fof(f3017,definition,
( spl122_504
<=> n13 = sum(n1,n12) ),
introduced(definition,[new_symbols(definition,[spl122_504])],[avatar_definition]) ).
fof(f3020,plain,
spl122_504,
inference(avatar_split_clause,[],[f473,f3017]) ).
fof(f3022,definition,
( spl122_505
<=> n12 = sum(n1,n11) ),
introduced(definition,[new_symbols(definition,[spl122_505])],[avatar_definition]) ).
fof(f3025,plain,
spl122_505,
inference(avatar_split_clause,[],[f474,f3022]) ).
fof(f3027,definition,
( spl122_506
<=> n11 = sum(n1,n10) ),
introduced(definition,[new_symbols(definition,[spl122_506])],[avatar_definition]) ).
fof(f3030,plain,
spl122_506,
inference(avatar_split_clause,[],[f475,f3027]) ).
fof(f3032,definition,
( spl122_507
<=> n10 = sum(n1,n9) ),
introduced(definition,[new_symbols(definition,[spl122_507])],[avatar_definition]) ).
fof(f3035,plain,
spl122_507,
inference(avatar_split_clause,[],[f476,f3032]) ).
fof(f3037,definition,
( spl122_508
<=> n9 = sum(n1,n8) ),
introduced(definition,[new_symbols(definition,[spl122_508])],[avatar_definition]) ).
fof(f3040,plain,
spl122_508,
inference(avatar_split_clause,[],[f477,f3037]) ).
fof(f3042,definition,
( spl122_509
<=> n8 = sum(n1,n7) ),
introduced(definition,[new_symbols(definition,[spl122_509])],[avatar_definition]) ).
fof(f3045,plain,
spl122_509,
inference(avatar_split_clause,[],[f478,f3042]) ).
fof(f3047,definition,
( spl122_510
<=> n7 = sum(n1,n6) ),
introduced(definition,[new_symbols(definition,[spl122_510])],[avatar_definition]) ).
fof(f3050,plain,
spl122_510,
inference(avatar_split_clause,[],[f479,f3047]) ).
fof(f3052,definition,
( spl122_511
<=> n6 = sum(n1,n5) ),
introduced(definition,[new_symbols(definition,[spl122_511])],[avatar_definition]) ).
fof(f3055,plain,
spl122_511,
inference(avatar_split_clause,[],[f480,f3052]) ).
fof(f3057,definition,
( spl122_512
<=> n5 = sum(n1,n4) ),
introduced(definition,[new_symbols(definition,[spl122_512])],[avatar_definition]) ).
fof(f3060,plain,
spl122_512,
inference(avatar_split_clause,[],[f481,f3057]) ).
fof(f3062,definition,
( spl122_513
<=> n4 = sum(n1,n3) ),
introduced(definition,[new_symbols(definition,[spl122_513])],[avatar_definition]) ).
fof(f3065,plain,
spl122_513,
inference(avatar_split_clause,[],[f482,f3062]) ).
fof(f3067,definition,
( spl122_514
<=> n3 = sum(n1,n2) ),
introduced(definition,[new_symbols(definition,[spl122_514])],[avatar_definition]) ).
fof(f3070,plain,
spl122_514,
inference(avatar_split_clause,[],[f483,f3067]) ).
fof(f3072,definition,
( spl122_515
<=> n2 = sum(n1,n1) ),
introduced(definition,[new_symbols(definition,[spl122_515])],[avatar_definition]) ).
fof(f3075,plain,
spl122_515,
inference(avatar_split_clause,[],[f484,f3072]) ).
fof(f3077,definition,
( spl122_516
<=> n1 = sum(n1,n0) ),
introduced(definition,[new_symbols(definition,[spl122_516])],[avatar_definition]) ).
fof(f3080,plain,
spl122_516,
inference(avatar_split_clause,[],[f485,f3077]) ).
fof(f3082,definition,
( spl122_517
<=> n15 = sum(n0,n15) ),
introduced(definition,[new_symbols(definition,[spl122_517])],[avatar_definition]) ).
fof(f3085,plain,
spl122_517,
inference(avatar_split_clause,[],[f486,f3082]) ).
fof(f3087,definition,
( spl122_518
<=> n14 = sum(n0,n14) ),
introduced(definition,[new_symbols(definition,[spl122_518])],[avatar_definition]) ).
fof(f3090,plain,
spl122_518,
inference(avatar_split_clause,[],[f487,f3087]) ).
fof(f3092,definition,
( spl122_519
<=> n13 = sum(n0,n13) ),
introduced(definition,[new_symbols(definition,[spl122_519])],[avatar_definition]) ).
fof(f3095,plain,
spl122_519,
inference(avatar_split_clause,[],[f488,f3092]) ).
fof(f3097,definition,
( spl122_520
<=> n12 = sum(n0,n12) ),
introduced(definition,[new_symbols(definition,[spl122_520])],[avatar_definition]) ).
fof(f3100,plain,
spl122_520,
inference(avatar_split_clause,[],[f489,f3097]) ).
fof(f3102,definition,
( spl122_521
<=> n11 = sum(n0,n11) ),
introduced(definition,[new_symbols(definition,[spl122_521])],[avatar_definition]) ).
fof(f3105,plain,
spl122_521,
inference(avatar_split_clause,[],[f490,f3102]) ).
fof(f3107,definition,
( spl122_522
<=> n10 = sum(n0,n10) ),
introduced(definition,[new_symbols(definition,[spl122_522])],[avatar_definition]) ).
fof(f3110,plain,
spl122_522,
inference(avatar_split_clause,[],[f491,f3107]) ).
fof(f3112,definition,
( spl122_523
<=> n9 = sum(n0,n9) ),
introduced(definition,[new_symbols(definition,[spl122_523])],[avatar_definition]) ).
fof(f3115,plain,
spl122_523,
inference(avatar_split_clause,[],[f492,f3112]) ).
fof(f3117,definition,
( spl122_524
<=> n8 = sum(n0,n8) ),
introduced(definition,[new_symbols(definition,[spl122_524])],[avatar_definition]) ).
fof(f3120,plain,
spl122_524,
inference(avatar_split_clause,[],[f493,f3117]) ).
fof(f3122,definition,
( spl122_525
<=> n7 = sum(n0,n7) ),
introduced(definition,[new_symbols(definition,[spl122_525])],[avatar_definition]) ).
fof(f3125,plain,
spl122_525,
inference(avatar_split_clause,[],[f494,f3122]) ).
fof(f3127,definition,
( spl122_526
<=> n6 = sum(n0,n6) ),
introduced(definition,[new_symbols(definition,[spl122_526])],[avatar_definition]) ).
fof(f3130,plain,
spl122_526,
inference(avatar_split_clause,[],[f495,f3127]) ).
fof(f3132,definition,
( spl122_527
<=> n5 = sum(n0,n5) ),
introduced(definition,[new_symbols(definition,[spl122_527])],[avatar_definition]) ).
fof(f3135,plain,
spl122_527,
inference(avatar_split_clause,[],[f496,f3132]) ).
fof(f3137,definition,
( spl122_528
<=> n4 = sum(n0,n4) ),
introduced(definition,[new_symbols(definition,[spl122_528])],[avatar_definition]) ).
fof(f3140,plain,
spl122_528,
inference(avatar_split_clause,[],[f497,f3137]) ).
fof(f3142,definition,
( spl122_529
<=> n3 = sum(n0,n3) ),
introduced(definition,[new_symbols(definition,[spl122_529])],[avatar_definition]) ).
fof(f3145,plain,
spl122_529,
inference(avatar_split_clause,[],[f498,f3142]) ).
fof(f3147,definition,
( spl122_530
<=> n2 = sum(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl122_530])],[avatar_definition]) ).
fof(f3150,plain,
spl122_530,
inference(avatar_split_clause,[],[f499,f3147]) ).
fof(f3152,definition,
( spl122_531
<=> n1 = sum(n0,n1) ),
introduced(definition,[new_symbols(definition,[spl122_531])],[avatar_definition]) ).
fof(f3155,plain,
spl122_531,
inference(avatar_split_clause,[],[f500,f3152]) ).
fof(f3157,definition,
( spl122_532
<=> n0 = sum(n0,n0) ),
introduced(definition,[new_symbols(definition,[spl122_532])],[avatar_definition]) ).
fof(f3160,plain,
spl122_532,
inference(avatar_split_clause,[],[f501,f3157]) ).
fof(f3162,definition,
( spl122_533
<=> n14 = pred(n15) ),
introduced(definition,[new_symbols(definition,[spl122_533])],[avatar_definition]) ).
fof(f3165,plain,
spl122_533,
inference(avatar_split_clause,[],[f502,f3162]) ).
fof(f3167,definition,
( spl122_534
<=> n13 = pred(n14) ),
introduced(definition,[new_symbols(definition,[spl122_534])],[avatar_definition]) ).
fof(f3170,plain,
spl122_534,
inference(avatar_split_clause,[],[f503,f3167]) ).
fof(f3172,definition,
( spl122_535
<=> n12 = pred(n13) ),
introduced(definition,[new_symbols(definition,[spl122_535])],[avatar_definition]) ).
fof(f3175,plain,
spl122_535,
inference(avatar_split_clause,[],[f504,f3172]) ).
fof(f3177,definition,
( spl122_536
<=> n11 = pred(n12) ),
introduced(definition,[new_symbols(definition,[spl122_536])],[avatar_definition]) ).
fof(f3180,plain,
spl122_536,
inference(avatar_split_clause,[],[f505,f3177]) ).
fof(f3182,definition,
( spl122_537
<=> n10 = pred(n11) ),
introduced(definition,[new_symbols(definition,[spl122_537])],[avatar_definition]) ).
fof(f3185,plain,
spl122_537,
inference(avatar_split_clause,[],[f506,f3182]) ).
fof(f3187,definition,
( spl122_538
<=> n9 = pred(n10) ),
introduced(definition,[new_symbols(definition,[spl122_538])],[avatar_definition]) ).
fof(f3190,plain,
spl122_538,
inference(avatar_split_clause,[],[f507,f3187]) ).
fof(f3192,definition,
( spl122_539
<=> n8 = pred(n9) ),
introduced(definition,[new_symbols(definition,[spl122_539])],[avatar_definition]) ).
fof(f3195,plain,
spl122_539,
inference(avatar_split_clause,[],[f508,f3192]) ).
fof(f3197,definition,
( spl122_540
<=> n7 = pred(n8) ),
introduced(definition,[new_symbols(definition,[spl122_540])],[avatar_definition]) ).
fof(f3200,plain,
spl122_540,
inference(avatar_split_clause,[],[f509,f3197]) ).
fof(f3202,definition,
( spl122_541
<=> n6 = pred(n7) ),
introduced(definition,[new_symbols(definition,[spl122_541])],[avatar_definition]) ).
fof(f3205,plain,
spl122_541,
inference(avatar_split_clause,[],[f510,f3202]) ).
fof(f3207,definition,
( spl122_542
<=> n5 = pred(n6) ),
introduced(definition,[new_symbols(definition,[spl122_542])],[avatar_definition]) ).
fof(f3210,plain,
spl122_542,
inference(avatar_split_clause,[],[f511,f3207]) ).
fof(f3212,definition,
( spl122_543
<=> n4 = pred(n5) ),
introduced(definition,[new_symbols(definition,[spl122_543])],[avatar_definition]) ).
fof(f3215,plain,
spl122_543,
inference(avatar_split_clause,[],[f512,f3212]) ).
fof(f3217,definition,
( spl122_544
<=> n3 = pred(n4) ),
introduced(definition,[new_symbols(definition,[spl122_544])],[avatar_definition]) ).
fof(f3220,plain,
spl122_544,
inference(avatar_split_clause,[],[f513,f3217]) ).
fof(f3222,definition,
( spl122_545
<=> n2 = pred(n3) ),
introduced(definition,[new_symbols(definition,[spl122_545])],[avatar_definition]) ).
fof(f3225,plain,
spl122_545,
inference(avatar_split_clause,[],[f514,f3222]) ).
fof(f3227,definition,
( spl122_546
<=> n1 = pred(n2) ),
introduced(definition,[new_symbols(definition,[spl122_546])],[avatar_definition]) ).
fof(f3230,plain,
spl122_546,
inference(avatar_split_clause,[],[f515,f3227]) ).
fof(f3232,definition,
( spl122_547
<=> n0 = pred(n1) ),
introduced(definition,[new_symbols(definition,[spl122_547])],[avatar_definition]) ).
fof(f3235,plain,
spl122_547,
inference(avatar_split_clause,[],[f516,f3232]) ).
fof(f3237,definition,
( spl122_548
<=> n15 = pred(n0) ),
introduced(definition,[new_symbols(definition,[spl122_548])],[avatar_definition]) ).
fof(f3240,plain,
spl122_548,
inference(avatar_split_clause,[],[f517,f3237]) ).
fof(f3242,definition,
( spl122_549
<=> n0 = succ(n15) ),
introduced(definition,[new_symbols(definition,[spl122_549])],[avatar_definition]) ).
fof(f3245,plain,
spl122_549,
inference(avatar_split_clause,[],[f518,f3242]) ).
fof(f3247,definition,
( spl122_550
<=> succ(n14) = n15 ),
introduced(definition,[new_symbols(definition,[spl122_550])],[avatar_definition]) ).
fof(f3250,plain,
spl122_550,
inference(avatar_split_clause,[],[f519,f3247]) ).
fof(f3252,definition,
( spl122_551
<=> succ(n13) = n14 ),
introduced(definition,[new_symbols(definition,[spl122_551])],[avatar_definition]) ).
fof(f3255,plain,
spl122_551,
inference(avatar_split_clause,[],[f520,f3252]) ).
fof(f3257,definition,
( spl122_552
<=> succ(n12) = n13 ),
introduced(definition,[new_symbols(definition,[spl122_552])],[avatar_definition]) ).
fof(f3260,plain,
spl122_552,
inference(avatar_split_clause,[],[f521,f3257]) ).
fof(f3262,definition,
( spl122_553
<=> succ(n11) = n12 ),
introduced(definition,[new_symbols(definition,[spl122_553])],[avatar_definition]) ).
fof(f3265,plain,
spl122_553,
inference(avatar_split_clause,[],[f522,f3262]) ).
fof(f3267,definition,
( spl122_554
<=> succ(n10) = n11 ),
introduced(definition,[new_symbols(definition,[spl122_554])],[avatar_definition]) ).
fof(f3270,plain,
spl122_554,
inference(avatar_split_clause,[],[f523,f3267]) ).
fof(f3272,definition,
( spl122_555
<=> succ(n9) = n10 ),
introduced(definition,[new_symbols(definition,[spl122_555])],[avatar_definition]) ).
fof(f3275,plain,
spl122_555,
inference(avatar_split_clause,[],[f524,f3272]) ).
fof(f3277,definition,
( spl122_556
<=> succ(n8) = n9 ),
introduced(definition,[new_symbols(definition,[spl122_556])],[avatar_definition]) ).
fof(f3280,plain,
spl122_556,
inference(avatar_split_clause,[],[f525,f3277]) ).
fof(f3282,definition,
( spl122_557
<=> succ(n7) = n8 ),
introduced(definition,[new_symbols(definition,[spl122_557])],[avatar_definition]) ).
fof(f3285,plain,
spl122_557,
inference(avatar_split_clause,[],[f526,f3282]) ).
fof(f3287,definition,
( spl122_558
<=> succ(n6) = n7 ),
introduced(definition,[new_symbols(definition,[spl122_558])],[avatar_definition]) ).
fof(f3290,plain,
spl122_558,
inference(avatar_split_clause,[],[f527,f3287]) ).
fof(f3292,definition,
( spl122_559
<=> succ(n5) = n6 ),
introduced(definition,[new_symbols(definition,[spl122_559])],[avatar_definition]) ).
fof(f3295,plain,
spl122_559,
inference(avatar_split_clause,[],[f528,f3292]) ).
fof(f3297,definition,
( spl122_560
<=> succ(n4) = n5 ),
introduced(definition,[new_symbols(definition,[spl122_560])],[avatar_definition]) ).
fof(f3300,plain,
spl122_560,
inference(avatar_split_clause,[],[f529,f3297]) ).
fof(f3302,definition,
( spl122_561
<=> succ(n3) = n4 ),
introduced(definition,[new_symbols(definition,[spl122_561])],[avatar_definition]) ).
fof(f3305,plain,
spl122_561,
inference(avatar_split_clause,[],[f530,f3302]) ).
fof(f3307,definition,
( spl122_562
<=> succ(n2) = n3 ),
introduced(definition,[new_symbols(definition,[spl122_562])],[avatar_definition]) ).
fof(f3310,plain,
spl122_562,
inference(avatar_split_clause,[],[f531,f3307]) ).
fof(f3312,definition,
( spl122_563
<=> succ(n1) = n2 ),
introduced(definition,[new_symbols(definition,[spl122_563])],[avatar_definition]) ).
fof(f3315,plain,
spl122_563,
inference(avatar_split_clause,[],[f532,f3312]) ).
fof(f3317,definition,
( spl122_564
<=>