%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM378+1.015.015 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:17 PM UTC 2026
% Result : Unsatisfiable 43.00s 6.96s
% Output : Refutation 0.24s
% 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] :
( 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 )
& X32 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X0))))))))))))))))
& X34 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X0))))))))))))))))
& X33 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X1))))))))))))))))
& X35 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X1))))))))))))))))
& X36 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X2))))))))))))))))
& X38 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X2))))))))))))))))
& X37 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X3))))))))))))))))
& X39 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X3))))))))))))))))
& X40 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X4))))))))))))))))
& X42 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X4))))))))))))))))
& X41 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X5))))))))))))))))
& X43 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X5))))))))))))))))
& X44 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X6))))))))))))))))
& X46 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X6))))))))))))))))
& X45 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X7))))))))))))))))
& X47 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X7))))))))))))))))
& X48 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X8))))))))))))))))
& X50 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X8))))))))))))))))
& X49 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X9))))))))))))))))
& X51 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X9))))))))))))))))
& X52 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X10))))))))))))))))
& X54 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X10))))))))))))))))
& X53 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X11))))))))))))))))
& X55 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X11))))))))))))))))
& X56 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X12))))))))))))))))
& X58 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X12))))))))))))))))
& X57 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X13))))))))))))))))
& X59 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X13))))))))))))))))
& X60 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X14))))))))))))))))
& X62 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X14))))))))))))))))
& X61 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X15))))))))))))))))
& X63 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X15))))))))))))))))
& X64 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X16))))))))))))))))
& X66 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X16))))))))))))))))
& X65 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X17))))))))))))))))
& X67 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X17))))))))))))))))
& X68 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X18))))))))))))))))
& X70 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X18))))))))))))))))
& X69 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X19))))))))))))))))
& X71 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X19))))))))))))))))
& X72 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X20))))))))))))))))
& X74 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X20))))))))))))))))
& X73 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X21))))))))))))))))
& X75 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X21))))))))))))))))
& X76 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X22))))))))))))))))
& X78 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X22))))))))))))))))
& X77 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X23))))))))))))))))
& X79 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X23))))))))))))))))
& X80 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X24))))))))))))))))
& X82 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X24))))))))))))))))
& X81 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X25))))))))))))))))
& X83 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X25))))))))))))))))
& X84 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X26))))))))))))))))
& X86 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X26))))))))))))))))
& X85 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X27))))))))))))))))
& X87 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X27))))))))))))))))
& X88 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X28))))))))))))))))
& X90 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X28))))))))))))))))
& X89 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(X29))))))))))))))))
& X91 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(X29))))))))))))))))
& X2 = sum(sum(pred(X0),succ(X1)),sum(pred(X1),succ(X0)))
& X3 = sum(pred(X34),sum(succ(X32),sum(pred(X35),succ(X33))))
& X4 = sum(sum(pred(X2),succ(X3)),sum(pred(X3),succ(X2)))
& X5 = sum(pred(X38),sum(succ(X36),sum(pred(X39),succ(X37))))
& X6 = sum(sum(pred(X4),succ(X5)),sum(pred(X5),succ(X4)))
& X7 = sum(pred(X42),sum(succ(X40),sum(pred(X43),succ(X41))))
& X8 = sum(sum(pred(X6),succ(X7)),sum(pred(X7),succ(X6)))
& X9 = sum(pred(X46),sum(succ(X44),sum(pred(X47),succ(X45))))
& X10 = sum(sum(pred(X8),succ(X9)),sum(pred(X9),succ(X8)))
& X11 = sum(pred(X50),sum(succ(X48),sum(pred(X51),succ(X49))))
& X12 = sum(sum(pred(X10),succ(X11)),sum(pred(X11),succ(X10)))
& X13 = sum(pred(X54),sum(succ(X52),sum(pred(X55),succ(X53))))
& X14 = sum(sum(pred(X12),succ(X13)),sum(pred(X13),succ(X12)))
& X15 = sum(pred(X58),sum(succ(X56),sum(pred(X59),succ(X57))))
& X16 = sum(sum(pred(X14),succ(X15)),sum(pred(X15),succ(X14)))
& X17 = sum(pred(X62),sum(succ(X60),sum(pred(X63),succ(X61))))
& X18 = sum(sum(pred(X16),succ(X17)),sum(pred(X17),succ(X16)))
& X19 = sum(pred(X66),sum(succ(X64),sum(pred(X67),succ(X65))))
& X20 = sum(sum(pred(X18),succ(X19)),sum(pred(X19),succ(X18)))
& X21 = sum(pred(X70),sum(succ(X68),sum(pred(X71),succ(X69))))
& X22 = sum(sum(pred(X20),succ(X21)),sum(pred(X21),succ(X20)))
& X23 = sum(pred(X74),sum(succ(X72),sum(pred(X75),succ(X73))))
& X24 = sum(sum(pred(X22),succ(X23)),sum(pred(X23),succ(X22)))
& X25 = sum(pred(X78),sum(succ(X76),sum(pred(X79),succ(X77))))
& X26 = sum(sum(pred(X24),succ(X25)),sum(pred(X25),succ(X24)))
& X27 = sum(pred(X82),sum(succ(X80),sum(pred(X83),succ(X81))))
& X28 = sum(sum(pred(X26),succ(X27)),sum(pred(X27),succ(X26)))
& X29 = sum(pred(X86),sum(succ(X84),sum(pred(X87),succ(X85))))
& X30 = sum(sum(pred(X28),succ(X29)),sum(pred(X29),succ(X28)))
& X31 = sum(pred(X90),sum(succ(X88),sum(pred(X91),succ(X89))))
& ( X24 != X25
| X26 != X27
| X28 != X29
| X30 != X31 )
& 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/sandbox2/benchmark/theBenchmark.p',try_satisfy_this) ).
fof(f2,plain,
( succ(n0) = n1
& succ(n1) = n2
& succ(n2) = n3
& succ(n3) = n4
& succ(n4) = n5
& succ(n5) = n6
& succ(n6) = n7
& succ(n7) = n8
& succ(n8) = n9
& succ(n9) = n10
& succ(n10) = 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 )
& sK32 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK0))))))))))))))))
& sK34 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK0))))))))))))))))
& sK33 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK1))))))))))))))))
& sK35 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK1))))))))))))))))
& sK36 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK2))))))))))))))))
& sK38 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK2))))))))))))))))
& sK37 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK3))))))))))))))))
& sK39 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK3))))))))))))))))
& sK40 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK4))))))))))))))))
& sK42 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK4))))))))))))))))
& sK41 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK5))))))))))))))))
& sK43 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK5))))))))))))))))
& sK44 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK6))))))))))))))))
& sK46 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK6))))))))))))))))
& sK45 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK7))))))))))))))))
& sK47 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK7))))))))))))))))
& sK48 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK8))))))))))))))))
& sK50 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK8))))))))))))))))
& sK49 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK9))))))))))))))))
& sK51 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK9))))))))))))))))
& sK52 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK10))))))))))))))))
& sK54 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK10))))))))))))))))
& sK53 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK11))))))))))))))))
& sK55 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK11))))))))))))))))
& sK56 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK12))))))))))))))))
& sK58 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK12))))))))))))))))
& sK57 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK13))))))))))))))))
& sK59 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK13))))))))))))))))
& sK60 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK14))))))))))))))))
& sK62 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK14))))))))))))))))
& sK61 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK15))))))))))))))))
& sK63 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK15))))))))))))))))
& sK64 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK16))))))))))))))))
& sK66 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK16))))))))))))))))
& sK65 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK17))))))))))))))))
& sK67 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK17))))))))))))))))
& sK68 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK18))))))))))))))))
& sK70 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK18))))))))))))))))
& sK69 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK19))))))))))))))))
& sK71 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK19))))))))))))))))
& sK72 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK20))))))))))))))))
& sK74 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK20))))))))))))))))
& sK73 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK21))))))))))))))))
& sK75 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK21))))))))))))))))
& sK76 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK22))))))))))))))))
& sK78 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK22))))))))))))))))
& sK77 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK23))))))))))))))))
& sK79 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK23))))))))))))))))
& sK80 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK24))))))))))))))))
& sK82 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK24))))))))))))))))
& sK81 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK25))))))))))))))))
& sK83 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK25))))))))))))))))
& sK84 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK26))))))))))))))))
& sK86 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK26))))))))))))))))
& sK85 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK27))))))))))))))))
& sK87 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK27))))))))))))))))
& sK88 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK28))))))))))))))))
& sK90 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK28))))))))))))))))
& sK89 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK29))))))))))))))))
& sK91 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK29))))))))))))))))
& sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0)))
& sK3 = sum(pred(sK34),sum(succ(sK32),sum(pred(sK35),succ(sK33))))
& sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2)))
& sK5 = sum(pred(sK38),sum(succ(sK36),sum(pred(sK39),succ(sK37))))
& sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4)))
& sK7 = sum(pred(sK42),sum(succ(sK40),sum(pred(sK43),succ(sK41))))
& sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6)))
& sK9 = sum(pred(sK46),sum(succ(sK44),sum(pred(sK47),succ(sK45))))
& sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8)))
& sK11 = sum(pred(sK50),sum(succ(sK48),sum(pred(sK51),succ(sK49))))
& sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10)))
& sK13 = sum(pred(sK54),sum(succ(sK52),sum(pred(sK55),succ(sK53))))
& sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12)))
& sK15 = sum(pred(sK58),sum(succ(sK56),sum(pred(sK59),succ(sK57))))
& sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14)))
& sK17 = sum(pred(sK62),sum(succ(sK60),sum(pred(sK63),succ(sK61))))
& sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16)))
& sK19 = sum(pred(sK66),sum(succ(sK64),sum(pred(sK67),succ(sK65))))
& sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18)))
& sK21 = sum(pred(sK70),sum(succ(sK68),sum(pred(sK71),succ(sK69))))
& sK22 = sum(sum(pred(sK20),succ(sK21)),sum(pred(sK21),succ(sK20)))
& sK23 = sum(pred(sK74),sum(succ(sK72),sum(pred(sK75),succ(sK73))))
& sK24 = sum(sum(pred(sK22),succ(sK23)),sum(pred(sK23),succ(sK22)))
& sK25 = sum(pred(sK78),sum(succ(sK76),sum(pred(sK79),succ(sK77))))
& sK26 = sum(sum(pred(sK24),succ(sK25)),sum(pred(sK25),succ(sK24)))
& sK27 = sum(pred(sK82),sum(succ(sK80),sum(pred(sK83),succ(sK81))))
& sK28 = sum(sum(pred(sK26),succ(sK27)),sum(pred(sK27),succ(sK26)))
& sK29 = sum(pred(sK86),sum(succ(sK84),sum(pred(sK87),succ(sK85))))
& sK30 = sum(sum(pred(sK28),succ(sK29)),sum(pred(sK29),succ(sK28)))
& sK31 = sum(pred(sK90),sum(succ(sK88),sum(pred(sK91),succ(sK89))))
& ( sK24 != sK25
| sK26 != sK27
| sK28 != sK29
| sK30 != sK31 )
& 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]),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)],[f1]) ).
fof(f123,plain,
( sK24 != sK25
| sK26 != sK27
| sK28 != sK29
| sK30 != sK31 ),
inference(cnf_transformation,[],[f2]) ).
fof(f124,plain,
sK31 = sum(pred(sK90),sum(succ(sK88),sum(pred(sK91),succ(sK89)))),
inference(cnf_transformation,[],[f2]) ).
fof(f125,plain,
sK30 = sum(sum(pred(sK28),succ(sK29)),sum(pred(sK29),succ(sK28))),
inference(cnf_transformation,[],[f2]) ).
fof(f126,plain,
sK29 = sum(pred(sK86),sum(succ(sK84),sum(pred(sK87),succ(sK85)))),
inference(cnf_transformation,[],[f2]) ).
fof(f127,plain,
sK28 = sum(sum(pred(sK26),succ(sK27)),sum(pred(sK27),succ(sK26))),
inference(cnf_transformation,[],[f2]) ).
fof(f128,plain,
sK27 = sum(pred(sK82),sum(succ(sK80),sum(pred(sK83),succ(sK81)))),
inference(cnf_transformation,[],[f2]) ).
fof(f129,plain,
sK26 = sum(sum(pred(sK24),succ(sK25)),sum(pred(sK25),succ(sK24))),
inference(cnf_transformation,[],[f2]) ).
fof(f130,plain,
sK25 = sum(pred(sK78),sum(succ(sK76),sum(pred(sK79),succ(sK77)))),
inference(cnf_transformation,[],[f2]) ).
fof(f131,plain,
sK24 = sum(sum(pred(sK22),succ(sK23)),sum(pred(sK23),succ(sK22))),
inference(cnf_transformation,[],[f2]) ).
fof(f132,plain,
sK23 = sum(pred(sK74),sum(succ(sK72),sum(pred(sK75),succ(sK73)))),
inference(cnf_transformation,[],[f2]) ).
fof(f133,plain,
sK22 = sum(sum(pred(sK20),succ(sK21)),sum(pred(sK21),succ(sK20))),
inference(cnf_transformation,[],[f2]) ).
fof(f134,plain,
sK21 = sum(pred(sK70),sum(succ(sK68),sum(pred(sK71),succ(sK69)))),
inference(cnf_transformation,[],[f2]) ).
fof(f135,plain,
sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18))),
inference(cnf_transformation,[],[f2]) ).
fof(f136,plain,
sK19 = sum(pred(sK66),sum(succ(sK64),sum(pred(sK67),succ(sK65)))),
inference(cnf_transformation,[],[f2]) ).
fof(f137,plain,
sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16))),
inference(cnf_transformation,[],[f2]) ).
fof(f138,plain,
sK17 = sum(pred(sK62),sum(succ(sK60),sum(pred(sK63),succ(sK61)))),
inference(cnf_transformation,[],[f2]) ).
fof(f139,plain,
sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14))),
inference(cnf_transformation,[],[f2]) ).
fof(f140,plain,
sK15 = sum(pred(sK58),sum(succ(sK56),sum(pred(sK59),succ(sK57)))),
inference(cnf_transformation,[],[f2]) ).
fof(f141,plain,
sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12))),
inference(cnf_transformation,[],[f2]) ).
fof(f142,plain,
sK13 = sum(pred(sK54),sum(succ(sK52),sum(pred(sK55),succ(sK53)))),
inference(cnf_transformation,[],[f2]) ).
fof(f143,plain,
sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10))),
inference(cnf_transformation,[],[f2]) ).
fof(f144,plain,
sK11 = sum(pred(sK50),sum(succ(sK48),sum(pred(sK51),succ(sK49)))),
inference(cnf_transformation,[],[f2]) ).
fof(f145,plain,
sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8))),
inference(cnf_transformation,[],[f2]) ).
fof(f146,plain,
sK9 = sum(pred(sK46),sum(succ(sK44),sum(pred(sK47),succ(sK45)))),
inference(cnf_transformation,[],[f2]) ).
fof(f147,plain,
sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6))),
inference(cnf_transformation,[],[f2]) ).
fof(f148,plain,
sK7 = sum(pred(sK42),sum(succ(sK40),sum(pred(sK43),succ(sK41)))),
inference(cnf_transformation,[],[f2]) ).
fof(f149,plain,
sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4))),
inference(cnf_transformation,[],[f2]) ).
fof(f150,plain,
sK5 = sum(pred(sK38),sum(succ(sK36),sum(pred(sK39),succ(sK37)))),
inference(cnf_transformation,[],[f2]) ).
fof(f151,plain,
sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2))),
inference(cnf_transformation,[],[f2]) ).
fof(f152,plain,
sK3 = sum(pred(sK34),sum(succ(sK32),sum(pred(sK35),succ(sK33)))),
inference(cnf_transformation,[],[f2]) ).
fof(f153,plain,
sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0))),
inference(cnf_transformation,[],[f2]) ).
fof(f154,plain,
sK91 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK29)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f155,plain,
sK89 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK29)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f156,plain,
sK90 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK28)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f157,plain,
sK88 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK28)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f158,plain,
sK87 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK27)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f159,plain,
sK85 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK27)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f160,plain,
sK86 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK26)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f161,plain,
sK84 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK26)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f162,plain,
sK83 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK25)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f163,plain,
sK81 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK25)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f164,plain,
sK82 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK24)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f165,plain,
sK80 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK24)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f166,plain,
sK79 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK23)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f167,plain,
sK77 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK23)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f168,plain,
sK78 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK22)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f169,plain,
sK76 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK22)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f170,plain,
sK75 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK21)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f171,plain,
sK73 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK21)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f172,plain,
sK74 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK20)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f173,plain,
sK72 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK20)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f174,plain,
sK71 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK19)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f175,plain,
sK69 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK19)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f176,plain,
sK70 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK18)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f177,plain,
sK68 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK18)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f178,plain,
sK67 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK17)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f179,plain,
sK65 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK17)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f180,plain,
sK66 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK16)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f181,plain,
sK64 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK16)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f182,plain,
sK63 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK15)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f183,plain,
sK61 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK15)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f184,plain,
sK62 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK14)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f185,plain,
sK60 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK14)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f186,plain,
sK59 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK13)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f187,plain,
sK57 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK13)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f188,plain,
sK58 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK12)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f189,plain,
sK56 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK12)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f190,plain,
sK55 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK11)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f191,plain,
sK53 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK11)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f192,plain,
sK54 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK10)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f193,plain,
sK52 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK10)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f194,plain,
sK51 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK9)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f195,plain,
sK49 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK9)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f196,plain,
sK50 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK8)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f197,plain,
sK48 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK8)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f198,plain,
sK47 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK7)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f199,plain,
sK45 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK7)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f200,plain,
sK46 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK6)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f201,plain,
sK44 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK6)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f202,plain,
sK43 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK5)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f203,plain,
sK41 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK5)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f204,plain,
sK42 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK4)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f205,plain,
sK40 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK4)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f206,plain,
sK39 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK3)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f207,plain,
sK37 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK3)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f208,plain,
sK38 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK2)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f209,plain,
sK36 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK2)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f210,plain,
sK35 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK1)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f211,plain,
sK33 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK1)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f212,plain,
sK34 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK0)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f213,plain,
sK32 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK0)))))))))))))))),
inference(cnf_transformation,[],[f2]) ).
fof(f214,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(f215,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(f216,plain,
n14 = sum(n15,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f217,plain,
n13 = sum(n15,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f218,plain,
n12 = sum(n15,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f219,plain,
n11 = sum(n15,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f220,plain,
n10 = sum(n15,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f221,plain,
n9 = sum(n15,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f222,plain,
n8 = sum(n15,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f223,plain,
n7 = sum(n15,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f224,plain,
n6 = sum(n15,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f225,plain,
n5 = sum(n15,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f226,plain,
n4 = sum(n15,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f227,plain,
n3 = sum(n15,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f228,plain,
n2 = sum(n15,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f229,plain,
n1 = sum(n15,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f230,plain,
n0 = sum(n15,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f231,plain,
n15 = sum(n15,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f232,plain,
n13 = sum(n14,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f233,plain,
n12 = sum(n14,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f234,plain,
n11 = sum(n14,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f235,plain,
n10 = sum(n14,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f236,plain,
n9 = sum(n14,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f237,plain,
n8 = sum(n14,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f238,plain,
n7 = sum(n14,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f239,plain,
n6 = sum(n14,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f240,plain,
n5 = sum(n14,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f241,plain,
n4 = sum(n14,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f242,plain,
n3 = sum(n14,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f243,plain,
n2 = sum(n14,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f244,plain,
n1 = sum(n14,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f245,plain,
n0 = sum(n14,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f246,plain,
n15 = sum(n14,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f247,plain,
n14 = sum(n14,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f248,plain,
n12 = sum(n13,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f249,plain,
n11 = sum(n13,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f250,plain,
n10 = sum(n13,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f251,plain,
n9 = sum(n13,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f252,plain,
n8 = sum(n13,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f253,plain,
n7 = sum(n13,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f254,plain,
n6 = sum(n13,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f255,plain,
n5 = sum(n13,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f256,plain,
n4 = sum(n13,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f257,plain,
n3 = sum(n13,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f258,plain,
n2 = sum(n13,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f259,plain,
n1 = sum(n13,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f260,plain,
n0 = sum(n13,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f261,plain,
n15 = sum(n13,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f262,plain,
n14 = sum(n13,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f263,plain,
n13 = sum(n13,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f264,plain,
n11 = sum(n12,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f265,plain,
n10 = sum(n12,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f266,plain,
n9 = sum(n12,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f267,plain,
n8 = sum(n12,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f268,plain,
n7 = sum(n12,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f269,plain,
n6 = sum(n12,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f270,plain,
n5 = sum(n12,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f271,plain,
n4 = sum(n12,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f272,plain,
n3 = sum(n12,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f273,plain,
n2 = sum(n12,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f274,plain,
n1 = sum(n12,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f275,plain,
n0 = sum(n12,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f276,plain,
n15 = sum(n12,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f277,plain,
n14 = sum(n12,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f278,plain,
n13 = sum(n12,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f279,plain,
n12 = sum(n12,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f280,plain,
n10 = sum(n11,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f281,plain,
n9 = sum(n11,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f282,plain,
n8 = sum(n11,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f283,plain,
n7 = sum(n11,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f284,plain,
n6 = sum(n11,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f285,plain,
n5 = sum(n11,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f286,plain,
n4 = sum(n11,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f287,plain,
n3 = sum(n11,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f288,plain,
n2 = sum(n11,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f289,plain,
n1 = sum(n11,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f290,plain,
n0 = sum(n11,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f291,plain,
n15 = sum(n11,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f292,plain,
n14 = sum(n11,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f293,plain,
n13 = sum(n11,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f294,plain,
n12 = sum(n11,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f295,plain,
n11 = sum(n11,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f296,plain,
n9 = sum(n10,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f297,plain,
n8 = sum(n10,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f298,plain,
n7 = sum(n10,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f299,plain,
n6 = sum(n10,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f300,plain,
n5 = sum(n10,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f301,plain,
n4 = sum(n10,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f302,plain,
n3 = sum(n10,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f303,plain,
n2 = sum(n10,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f304,plain,
n1 = sum(n10,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f305,plain,
n0 = sum(n10,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f306,plain,
n15 = sum(n10,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f307,plain,
n14 = sum(n10,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f308,plain,
n13 = sum(n10,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f309,plain,
n12 = sum(n10,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f310,plain,
n11 = sum(n10,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f311,plain,
n10 = sum(n10,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f312,plain,
n8 = sum(n9,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f313,plain,
n7 = sum(n9,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f314,plain,
n6 = sum(n9,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f315,plain,
n5 = sum(n9,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f316,plain,
n4 = sum(n9,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f317,plain,
n3 = sum(n9,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f318,plain,
n2 = sum(n9,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f319,plain,
n1 = sum(n9,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f320,plain,
n0 = sum(n9,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f321,plain,
n15 = sum(n9,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f322,plain,
n14 = sum(n9,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f323,plain,
n13 = sum(n9,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f324,plain,
n12 = sum(n9,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f325,plain,
n11 = sum(n9,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f326,plain,
n10 = sum(n9,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f327,plain,
n9 = sum(n9,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f328,plain,
n7 = sum(n8,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f329,plain,
n6 = sum(n8,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f330,plain,
n5 = sum(n8,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f331,plain,
n4 = sum(n8,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f332,plain,
n3 = sum(n8,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f333,plain,
n2 = sum(n8,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f334,plain,
n1 = sum(n8,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f335,plain,
n0 = sum(n8,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f336,plain,
n15 = sum(n8,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f337,plain,
n14 = sum(n8,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f338,plain,
n13 = sum(n8,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f339,plain,
n12 = sum(n8,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f340,plain,
n11 = sum(n8,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f341,plain,
n10 = sum(n8,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f342,plain,
n9 = sum(n8,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f343,plain,
n8 = sum(n8,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f344,plain,
n6 = sum(n7,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f345,plain,
n5 = sum(n7,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f346,plain,
n4 = sum(n7,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f347,plain,
n3 = sum(n7,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f348,plain,
n2 = sum(n7,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f349,plain,
n1 = sum(n7,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f350,plain,
n0 = sum(n7,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f351,plain,
n15 = sum(n7,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f352,plain,
n14 = sum(n7,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f353,plain,
n13 = sum(n7,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f354,plain,
n12 = sum(n7,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f355,plain,
n11 = sum(n7,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f356,plain,
n10 = sum(n7,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f357,plain,
n9 = sum(n7,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f358,plain,
n8 = sum(n7,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f359,plain,
n7 = sum(n7,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f360,plain,
n5 = sum(n6,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f361,plain,
n4 = sum(n6,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f362,plain,
n3 = sum(n6,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f363,plain,
n2 = sum(n6,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f364,plain,
n1 = sum(n6,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f365,plain,
n0 = sum(n6,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f366,plain,
n15 = sum(n6,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f367,plain,
n14 = sum(n6,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f368,plain,
n13 = sum(n6,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f369,plain,
n12 = sum(n6,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f370,plain,
n11 = sum(n6,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f371,plain,
n10 = sum(n6,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f372,plain,
n9 = sum(n6,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f373,plain,
n8 = sum(n6,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f374,plain,
n7 = sum(n6,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f375,plain,
n6 = sum(n6,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f376,plain,
n4 = sum(n5,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f377,plain,
n3 = sum(n5,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f378,plain,
n2 = sum(n5,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f379,plain,
n1 = sum(n5,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f380,plain,
n0 = sum(n5,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f381,plain,
n15 = sum(n5,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f382,plain,
n14 = sum(n5,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f383,plain,
n13 = sum(n5,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f384,plain,
n12 = sum(n5,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f385,plain,
n11 = sum(n5,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f386,plain,
n10 = sum(n5,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f387,plain,
n9 = sum(n5,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f388,plain,
n8 = sum(n5,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f389,plain,
n7 = sum(n5,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f390,plain,
n6 = sum(n5,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f391,plain,
n5 = sum(n5,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f392,plain,
n3 = sum(n4,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f393,plain,
n2 = sum(n4,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f394,plain,
n1 = sum(n4,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f395,plain,
n0 = sum(n4,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f396,plain,
n15 = sum(n4,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f397,plain,
n14 = sum(n4,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f398,plain,
n13 = sum(n4,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f399,plain,
n12 = sum(n4,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f400,plain,
n11 = sum(n4,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f401,plain,
n10 = sum(n4,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f402,plain,
n9 = sum(n4,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f403,plain,
n8 = sum(n4,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f404,plain,
n7 = sum(n4,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f405,plain,
n6 = sum(n4,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f406,plain,
n5 = sum(n4,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f407,plain,
n4 = sum(n4,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f408,plain,
n2 = sum(n3,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f409,plain,
n1 = sum(n3,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f410,plain,
n0 = sum(n3,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f411,plain,
n15 = sum(n3,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f412,plain,
n14 = sum(n3,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f413,plain,
n13 = sum(n3,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f414,plain,
n12 = sum(n3,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f415,plain,
n11 = sum(n3,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f416,plain,
n10 = sum(n3,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f417,plain,
n9 = sum(n3,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f418,plain,
n8 = sum(n3,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f419,plain,
n7 = sum(n3,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f420,plain,
n6 = sum(n3,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f421,plain,
n5 = sum(n3,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f422,plain,
n4 = sum(n3,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f423,plain,
n3 = sum(n3,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f424,plain,
n1 = sum(n2,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f425,plain,
n0 = sum(n2,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f426,plain,
n15 = sum(n2,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f427,plain,
n14 = sum(n2,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f428,plain,
n13 = sum(n2,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f429,plain,
n12 = sum(n2,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f430,plain,
n11 = sum(n2,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f431,plain,
n10 = sum(n2,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f432,plain,
n9 = sum(n2,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f433,plain,
n8 = sum(n2,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f434,plain,
n7 = sum(n2,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f435,plain,
n6 = sum(n2,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f436,plain,
n5 = sum(n2,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f437,plain,
n4 = sum(n2,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f438,plain,
n3 = sum(n2,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f439,plain,
n2 = sum(n2,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f440,plain,
n0 = sum(n1,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f441,plain,
n15 = sum(n1,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f442,plain,
n14 = sum(n1,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f443,plain,
n13 = sum(n1,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f444,plain,
n12 = sum(n1,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f445,plain,
n11 = sum(n1,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f446,plain,
n10 = sum(n1,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f447,plain,
n9 = sum(n1,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f448,plain,
n8 = sum(n1,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f449,plain,
n7 = sum(n1,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f450,plain,
n6 = sum(n1,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f451,plain,
n5 = sum(n1,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f452,plain,
n4 = sum(n1,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f453,plain,
n3 = sum(n1,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f454,plain,
n2 = sum(n1,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f455,plain,
n1 = sum(n1,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f456,plain,
n15 = sum(n0,n15),
inference(cnf_transformation,[],[f2]) ).
fof(f457,plain,
n14 = sum(n0,n14),
inference(cnf_transformation,[],[f2]) ).
fof(f458,plain,
n13 = sum(n0,n13),
inference(cnf_transformation,[],[f2]) ).
fof(f459,plain,
n12 = sum(n0,n12),
inference(cnf_transformation,[],[f2]) ).
fof(f460,plain,
n11 = sum(n0,n11),
inference(cnf_transformation,[],[f2]) ).
fof(f461,plain,
n10 = sum(n0,n10),
inference(cnf_transformation,[],[f2]) ).
fof(f462,plain,
n9 = sum(n0,n9),
inference(cnf_transformation,[],[f2]) ).
fof(f463,plain,
n8 = sum(n0,n8),
inference(cnf_transformation,[],[f2]) ).
fof(f464,plain,
n7 = sum(n0,n7),
inference(cnf_transformation,[],[f2]) ).
fof(f465,plain,
n6 = sum(n0,n6),
inference(cnf_transformation,[],[f2]) ).
fof(f466,plain,
n5 = sum(n0,n5),
inference(cnf_transformation,[],[f2]) ).
fof(f467,plain,
n4 = sum(n0,n4),
inference(cnf_transformation,[],[f2]) ).
fof(f468,plain,
n3 = sum(n0,n3),
inference(cnf_transformation,[],[f2]) ).
fof(f469,plain,
n2 = sum(n0,n2),
inference(cnf_transformation,[],[f2]) ).
fof(f470,plain,
n1 = sum(n0,n1),
inference(cnf_transformation,[],[f2]) ).
fof(f471,plain,
n0 = sum(n0,n0),
inference(cnf_transformation,[],[f2]) ).
fof(f472,plain,
n14 = pred(n15),
inference(cnf_transformation,[],[f2]) ).
fof(f473,plain,
n13 = pred(n14),
inference(cnf_transformation,[],[f2]) ).
fof(f474,plain,
n12 = pred(n13),
inference(cnf_transformation,[],[f2]) ).
fof(f475,plain,
n11 = pred(n12),
inference(cnf_transformation,[],[f2]) ).
fof(f476,plain,
n10 = pred(n11),
inference(cnf_transformation,[],[f2]) ).
fof(f477,plain,
n9 = pred(n10),
inference(cnf_transformation,[],[f2]) ).
fof(f478,plain,
n8 = pred(n9),
inference(cnf_transformation,[],[f2]) ).
fof(f479,plain,
n7 = pred(n8),
inference(cnf_transformation,[],[f2]) ).
fof(f480,plain,
n6 = pred(n7),
inference(cnf_transformation,[],[f2]) ).
fof(f481,plain,
n5 = pred(n6),
inference(cnf_transformation,[],[f2]) ).
fof(f482,plain,
n4 = pred(n5),
inference(cnf_transformation,[],[f2]) ).
fof(f483,plain,
n3 = pred(n4),
inference(cnf_transformation,[],[f2]) ).
fof(f484,plain,
n2 = pred(n3),
inference(cnf_transformation,[],[f2]) ).
fof(f485,plain,
n1 = pred(n2),
inference(cnf_transformation,[],[f2]) ).
fof(f486,plain,
n0 = pred(n1),
inference(cnf_transformation,[],[f2]) ).
fof(f487,plain,
n15 = pred(n0),
inference(cnf_transformation,[],[f2]) ).
fof(f488,plain,
n0 = succ(n15),
inference(cnf_transformation,[],[f2]) ).
fof(f489,plain,
succ(n14) = n15,
inference(cnf_transformation,[],[f2]) ).
fof(f490,plain,
succ(n13) = n14,
inference(cnf_transformation,[],[f2]) ).
fof(f491,plain,
succ(n12) = n13,
inference(cnf_transformation,[],[f2]) ).
fof(f492,plain,
succ(n11) = n12,
inference(cnf_transformation,[],[f2]) ).
fof(f493,plain,
succ(n10) = n11,
inference(cnf_transformation,[],[f2]) ).
fof(f494,plain,
succ(n9) = n10,
inference(cnf_transformation,[],[f2]) ).
fof(f495,plain,
succ(n8) = n9,
inference(cnf_transformation,[],[f2]) ).
fof(f496,plain,
succ(n7) = n8,
inference(cnf_transformation,[],[f2]) ).
fof(f497,plain,
succ(n6) = n7,
inference(cnf_transformation,[],[f2]) ).
fof(f498,plain,
succ(n5) = n6,
inference(cnf_transformation,[],[f2]) ).
fof(f499,plain,
succ(n4) = n5,
inference(cnf_transformation,[],[f2]) ).
fof(f500,plain,
succ(n3) = n4,
inference(cnf_transformation,[],[f2]) ).
fof(f501,plain,
succ(n2) = n3,
inference(cnf_transformation,[],[f2]) ).
fof(f502,plain,
succ(n1) = n2,
inference(cnf_transformation,[],[f2]) ).
fof(f503,plain,
succ(n0) = n1,
inference(cnf_transformation,[],[f2]) ).
fof(f1105,definition,
( spl92_121
<=> sK30 = sK31 ),
introduced(definition,[new_symbols(definition,[spl92_121])],[avatar_definition]) ).
fof(f1109,definition,
( spl92_122
<=> sK28 = sK29 ),
introduced(definition,[new_symbols(definition,[spl92_122])],[avatar_definition]) ).
fof(f1113,definition,
( spl92_123
<=> sK26 = sK27 ),
introduced(definition,[new_symbols(definition,[spl92_123])],[avatar_definition]) ).
fof(f1117,definition,
( spl92_124
<=> sK24 = sK25 ),
introduced(definition,[new_symbols(definition,[spl92_124])],[avatar_definition]) ).
fof(f1120,plain,
( ~ spl92_121
| ~ spl92_122
| ~ spl92_123
| ~ spl92_124 ),
inference(avatar_split_clause,[],[f123,f1117,f1113,f1109,f1105]) ).
fof(f1122,definition,
( spl92_125
<=> sK31 = sum(pred(sK90),sum(succ(sK88),sum(pred(sK91),succ(sK89)))) ),
introduced(definition,[new_symbols(definition,[spl92_125])],[avatar_definition]) ).
fof(f1125,plain,
spl92_125,
inference(avatar_split_clause,[],[f124,f1122]) ).
fof(f1127,definition,
( spl92_126
<=> sK30 = sum(sum(pred(sK28),succ(sK29)),sum(pred(sK29),succ(sK28))) ),
introduced(definition,[new_symbols(definition,[spl92_126])],[avatar_definition]) ).
fof(f1130,plain,
spl92_126,
inference(avatar_split_clause,[],[f125,f1127]) ).
fof(f1132,definition,
( spl92_127
<=> sK29 = sum(pred(sK86),sum(succ(sK84),sum(pred(sK87),succ(sK85)))) ),
introduced(definition,[new_symbols(definition,[spl92_127])],[avatar_definition]) ).
fof(f1135,plain,
spl92_127,
inference(avatar_split_clause,[],[f126,f1132]) ).
fof(f1137,definition,
( spl92_128
<=> sK28 = sum(sum(pred(sK26),succ(sK27)),sum(pred(sK27),succ(sK26))) ),
introduced(definition,[new_symbols(definition,[spl92_128])],[avatar_definition]) ).
fof(f1140,plain,
spl92_128,
inference(avatar_split_clause,[],[f127,f1137]) ).
fof(f1142,definition,
( spl92_129
<=> sK27 = sum(pred(sK82),sum(succ(sK80),sum(pred(sK83),succ(sK81)))) ),
introduced(definition,[new_symbols(definition,[spl92_129])],[avatar_definition]) ).
fof(f1145,plain,
spl92_129,
inference(avatar_split_clause,[],[f128,f1142]) ).
fof(f1147,definition,
( spl92_130
<=> sK26 = sum(sum(pred(sK24),succ(sK25)),sum(pred(sK25),succ(sK24))) ),
introduced(definition,[new_symbols(definition,[spl92_130])],[avatar_definition]) ).
fof(f1150,plain,
spl92_130,
inference(avatar_split_clause,[],[f129,f1147]) ).
fof(f1152,definition,
( spl92_131
<=> sK25 = sum(pred(sK78),sum(succ(sK76),sum(pred(sK79),succ(sK77)))) ),
introduced(definition,[new_symbols(definition,[spl92_131])],[avatar_definition]) ).
fof(f1155,plain,
spl92_131,
inference(avatar_split_clause,[],[f130,f1152]) ).
fof(f1157,definition,
( spl92_132
<=> sK24 = sum(sum(pred(sK22),succ(sK23)),sum(pred(sK23),succ(sK22))) ),
introduced(definition,[new_symbols(definition,[spl92_132])],[avatar_definition]) ).
fof(f1160,plain,
spl92_132,
inference(avatar_split_clause,[],[f131,f1157]) ).
fof(f1162,definition,
( spl92_133
<=> sK23 = sum(pred(sK74),sum(succ(sK72),sum(pred(sK75),succ(sK73)))) ),
introduced(definition,[new_symbols(definition,[spl92_133])],[avatar_definition]) ).
fof(f1165,plain,
spl92_133,
inference(avatar_split_clause,[],[f132,f1162]) ).
fof(f1167,definition,
( spl92_134
<=> sK22 = sum(sum(pred(sK20),succ(sK21)),sum(pred(sK21),succ(sK20))) ),
introduced(definition,[new_symbols(definition,[spl92_134])],[avatar_definition]) ).
fof(f1170,plain,
spl92_134,
inference(avatar_split_clause,[],[f133,f1167]) ).
fof(f1172,definition,
( spl92_135
<=> sK21 = sum(pred(sK70),sum(succ(sK68),sum(pred(sK71),succ(sK69)))) ),
introduced(definition,[new_symbols(definition,[spl92_135])],[avatar_definition]) ).
fof(f1175,plain,
spl92_135,
inference(avatar_split_clause,[],[f134,f1172]) ).
fof(f1177,definition,
( spl92_136
<=> sK20 = sum(sum(pred(sK18),succ(sK19)),sum(pred(sK19),succ(sK18))) ),
introduced(definition,[new_symbols(definition,[spl92_136])],[avatar_definition]) ).
fof(f1180,plain,
spl92_136,
inference(avatar_split_clause,[],[f135,f1177]) ).
fof(f1182,definition,
( spl92_137
<=> sK19 = sum(pred(sK66),sum(succ(sK64),sum(pred(sK67),succ(sK65)))) ),
introduced(definition,[new_symbols(definition,[spl92_137])],[avatar_definition]) ).
fof(f1185,plain,
spl92_137,
inference(avatar_split_clause,[],[f136,f1182]) ).
fof(f1187,definition,
( spl92_138
<=> sK18 = sum(sum(pred(sK16),succ(sK17)),sum(pred(sK17),succ(sK16))) ),
introduced(definition,[new_symbols(definition,[spl92_138])],[avatar_definition]) ).
fof(f1190,plain,
spl92_138,
inference(avatar_split_clause,[],[f137,f1187]) ).
fof(f1192,definition,
( spl92_139
<=> sK17 = sum(pred(sK62),sum(succ(sK60),sum(pred(sK63),succ(sK61)))) ),
introduced(definition,[new_symbols(definition,[spl92_139])],[avatar_definition]) ).
fof(f1195,plain,
spl92_139,
inference(avatar_split_clause,[],[f138,f1192]) ).
fof(f1197,definition,
( spl92_140
<=> sK16 = sum(sum(pred(sK14),succ(sK15)),sum(pred(sK15),succ(sK14))) ),
introduced(definition,[new_symbols(definition,[spl92_140])],[avatar_definition]) ).
fof(f1200,plain,
spl92_140,
inference(avatar_split_clause,[],[f139,f1197]) ).
fof(f1202,definition,
( spl92_141
<=> sK15 = sum(pred(sK58),sum(succ(sK56),sum(pred(sK59),succ(sK57)))) ),
introduced(definition,[new_symbols(definition,[spl92_141])],[avatar_definition]) ).
fof(f1205,plain,
spl92_141,
inference(avatar_split_clause,[],[f140,f1202]) ).
fof(f1207,definition,
( spl92_142
<=> sK14 = sum(sum(pred(sK12),succ(sK13)),sum(pred(sK13),succ(sK12))) ),
introduced(definition,[new_symbols(definition,[spl92_142])],[avatar_definition]) ).
fof(f1210,plain,
spl92_142,
inference(avatar_split_clause,[],[f141,f1207]) ).
fof(f1212,definition,
( spl92_143
<=> sK13 = sum(pred(sK54),sum(succ(sK52),sum(pred(sK55),succ(sK53)))) ),
introduced(definition,[new_symbols(definition,[spl92_143])],[avatar_definition]) ).
fof(f1215,plain,
spl92_143,
inference(avatar_split_clause,[],[f142,f1212]) ).
fof(f1217,definition,
( spl92_144
<=> sK12 = sum(sum(pred(sK10),succ(sK11)),sum(pred(sK11),succ(sK10))) ),
introduced(definition,[new_symbols(definition,[spl92_144])],[avatar_definition]) ).
fof(f1220,plain,
spl92_144,
inference(avatar_split_clause,[],[f143,f1217]) ).
fof(f1222,definition,
( spl92_145
<=> sK11 = sum(pred(sK50),sum(succ(sK48),sum(pred(sK51),succ(sK49)))) ),
introduced(definition,[new_symbols(definition,[spl92_145])],[avatar_definition]) ).
fof(f1225,plain,
spl92_145,
inference(avatar_split_clause,[],[f144,f1222]) ).
fof(f1227,definition,
( spl92_146
<=> sK10 = sum(sum(pred(sK8),succ(sK9)),sum(pred(sK9),succ(sK8))) ),
introduced(definition,[new_symbols(definition,[spl92_146])],[avatar_definition]) ).
fof(f1230,plain,
spl92_146,
inference(avatar_split_clause,[],[f145,f1227]) ).
fof(f1232,definition,
( spl92_147
<=> sK9 = sum(pred(sK46),sum(succ(sK44),sum(pred(sK47),succ(sK45)))) ),
introduced(definition,[new_symbols(definition,[spl92_147])],[avatar_definition]) ).
fof(f1235,plain,
spl92_147,
inference(avatar_split_clause,[],[f146,f1232]) ).
fof(f1237,definition,
( spl92_148
<=> sK8 = sum(sum(pred(sK6),succ(sK7)),sum(pred(sK7),succ(sK6))) ),
introduced(definition,[new_symbols(definition,[spl92_148])],[avatar_definition]) ).
fof(f1240,plain,
spl92_148,
inference(avatar_split_clause,[],[f147,f1237]) ).
fof(f1242,definition,
( spl92_149
<=> sK7 = sum(pred(sK42),sum(succ(sK40),sum(pred(sK43),succ(sK41)))) ),
introduced(definition,[new_symbols(definition,[spl92_149])],[avatar_definition]) ).
fof(f1245,plain,
spl92_149,
inference(avatar_split_clause,[],[f148,f1242]) ).
fof(f1247,definition,
( spl92_150
<=> sK6 = sum(sum(pred(sK4),succ(sK5)),sum(pred(sK5),succ(sK4))) ),
introduced(definition,[new_symbols(definition,[spl92_150])],[avatar_definition]) ).
fof(f1250,plain,
spl92_150,
inference(avatar_split_clause,[],[f149,f1247]) ).
fof(f1252,definition,
( spl92_151
<=> sK5 = sum(pred(sK38),sum(succ(sK36),sum(pred(sK39),succ(sK37)))) ),
introduced(definition,[new_symbols(definition,[spl92_151])],[avatar_definition]) ).
fof(f1255,plain,
spl92_151,
inference(avatar_split_clause,[],[f150,f1252]) ).
fof(f1257,definition,
( spl92_152
<=> sK4 = sum(sum(pred(sK2),succ(sK3)),sum(pred(sK3),succ(sK2))) ),
introduced(definition,[new_symbols(definition,[spl92_152])],[avatar_definition]) ).
fof(f1260,plain,
spl92_152,
inference(avatar_split_clause,[],[f151,f1257]) ).
fof(f1262,definition,
( spl92_153
<=> sK3 = sum(pred(sK34),sum(succ(sK32),sum(pred(sK35),succ(sK33)))) ),
introduced(definition,[new_symbols(definition,[spl92_153])],[avatar_definition]) ).
fof(f1265,plain,
spl92_153,
inference(avatar_split_clause,[],[f152,f1262]) ).
fof(f1267,definition,
( spl92_154
<=> sK2 = sum(sum(pred(sK0),succ(sK1)),sum(pred(sK1),succ(sK0))) ),
introduced(definition,[new_symbols(definition,[spl92_154])],[avatar_definition]) ).
fof(f1270,plain,
spl92_154,
inference(avatar_split_clause,[],[f153,f1267]) ).
fof(f1272,definition,
( spl92_155
<=> sK91 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK29)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_155])],[avatar_definition]) ).
fof(f1275,plain,
spl92_155,
inference(avatar_split_clause,[],[f154,f1272]) ).
fof(f1277,definition,
( spl92_156
<=> sK89 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK29)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_156])],[avatar_definition]) ).
fof(f1280,plain,
spl92_156,
inference(avatar_split_clause,[],[f155,f1277]) ).
fof(f1282,definition,
( spl92_157
<=> sK90 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK28)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_157])],[avatar_definition]) ).
fof(f1285,plain,
spl92_157,
inference(avatar_split_clause,[],[f156,f1282]) ).
fof(f1287,definition,
( spl92_158
<=> sK88 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK28)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_158])],[avatar_definition]) ).
fof(f1290,plain,
spl92_158,
inference(avatar_split_clause,[],[f157,f1287]) ).
fof(f1292,definition,
( spl92_159
<=> sK87 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK27)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_159])],[avatar_definition]) ).
fof(f1295,plain,
spl92_159,
inference(avatar_split_clause,[],[f158,f1292]) ).
fof(f1297,definition,
( spl92_160
<=> sK85 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK27)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_160])],[avatar_definition]) ).
fof(f1300,plain,
spl92_160,
inference(avatar_split_clause,[],[f159,f1297]) ).
fof(f1302,definition,
( spl92_161
<=> sK86 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK26)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_161])],[avatar_definition]) ).
fof(f1305,plain,
spl92_161,
inference(avatar_split_clause,[],[f160,f1302]) ).
fof(f1307,definition,
( spl92_162
<=> sK84 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK26)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_162])],[avatar_definition]) ).
fof(f1310,plain,
spl92_162,
inference(avatar_split_clause,[],[f161,f1307]) ).
fof(f1312,definition,
( spl92_163
<=> sK83 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK25)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_163])],[avatar_definition]) ).
fof(f1315,plain,
spl92_163,
inference(avatar_split_clause,[],[f162,f1312]) ).
fof(f1317,definition,
( spl92_164
<=> sK81 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK25)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_164])],[avatar_definition]) ).
fof(f1320,plain,
spl92_164,
inference(avatar_split_clause,[],[f163,f1317]) ).
fof(f1322,definition,
( spl92_165
<=> sK82 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK24)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_165])],[avatar_definition]) ).
fof(f1325,plain,
spl92_165,
inference(avatar_split_clause,[],[f164,f1322]) ).
fof(f1327,definition,
( spl92_166
<=> sK80 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK24)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_166])],[avatar_definition]) ).
fof(f1330,plain,
spl92_166,
inference(avatar_split_clause,[],[f165,f1327]) ).
fof(f1332,definition,
( spl92_167
<=> sK79 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK23)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_167])],[avatar_definition]) ).
fof(f1335,plain,
spl92_167,
inference(avatar_split_clause,[],[f166,f1332]) ).
fof(f1337,definition,
( spl92_168
<=> sK77 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK23)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_168])],[avatar_definition]) ).
fof(f1340,plain,
spl92_168,
inference(avatar_split_clause,[],[f167,f1337]) ).
fof(f1342,definition,
( spl92_169
<=> sK78 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK22)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_169])],[avatar_definition]) ).
fof(f1345,plain,
spl92_169,
inference(avatar_split_clause,[],[f168,f1342]) ).
fof(f1347,definition,
( spl92_170
<=> sK76 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK22)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_170])],[avatar_definition]) ).
fof(f1350,plain,
spl92_170,
inference(avatar_split_clause,[],[f169,f1347]) ).
fof(f1352,definition,
( spl92_171
<=> sK75 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK21)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_171])],[avatar_definition]) ).
fof(f1355,plain,
spl92_171,
inference(avatar_split_clause,[],[f170,f1352]) ).
fof(f1357,definition,
( spl92_172
<=> sK73 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK21)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_172])],[avatar_definition]) ).
fof(f1360,plain,
spl92_172,
inference(avatar_split_clause,[],[f171,f1357]) ).
fof(f1362,definition,
( spl92_173
<=> sK74 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK20)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_173])],[avatar_definition]) ).
fof(f1365,plain,
spl92_173,
inference(avatar_split_clause,[],[f172,f1362]) ).
fof(f1367,definition,
( spl92_174
<=> sK72 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK20)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_174])],[avatar_definition]) ).
fof(f1370,plain,
spl92_174,
inference(avatar_split_clause,[],[f173,f1367]) ).
fof(f1372,definition,
( spl92_175
<=> sK71 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK19)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_175])],[avatar_definition]) ).
fof(f1375,plain,
spl92_175,
inference(avatar_split_clause,[],[f174,f1372]) ).
fof(f1377,definition,
( spl92_176
<=> sK69 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK19)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_176])],[avatar_definition]) ).
fof(f1380,plain,
spl92_176,
inference(avatar_split_clause,[],[f175,f1377]) ).
fof(f1382,definition,
( spl92_177
<=> sK70 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK18)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_177])],[avatar_definition]) ).
fof(f1385,plain,
spl92_177,
inference(avatar_split_clause,[],[f176,f1382]) ).
fof(f1387,definition,
( spl92_178
<=> sK68 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK18)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_178])],[avatar_definition]) ).
fof(f1390,plain,
spl92_178,
inference(avatar_split_clause,[],[f177,f1387]) ).
fof(f1392,definition,
( spl92_179
<=> sK67 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK17)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_179])],[avatar_definition]) ).
fof(f1395,plain,
spl92_179,
inference(avatar_split_clause,[],[f178,f1392]) ).
fof(f1397,definition,
( spl92_180
<=> sK65 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK17)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_180])],[avatar_definition]) ).
fof(f1400,plain,
spl92_180,
inference(avatar_split_clause,[],[f179,f1397]) ).
fof(f1402,definition,
( spl92_181
<=> sK66 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK16)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_181])],[avatar_definition]) ).
fof(f1405,plain,
spl92_181,
inference(avatar_split_clause,[],[f180,f1402]) ).
fof(f1407,definition,
( spl92_182
<=> sK64 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK16)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_182])],[avatar_definition]) ).
fof(f1410,plain,
spl92_182,
inference(avatar_split_clause,[],[f181,f1407]) ).
fof(f1412,definition,
( spl92_183
<=> sK63 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK15)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_183])],[avatar_definition]) ).
fof(f1415,plain,
spl92_183,
inference(avatar_split_clause,[],[f182,f1412]) ).
fof(f1417,definition,
( spl92_184
<=> sK61 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK15)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_184])],[avatar_definition]) ).
fof(f1420,plain,
spl92_184,
inference(avatar_split_clause,[],[f183,f1417]) ).
fof(f1422,definition,
( spl92_185
<=> sK62 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK14)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_185])],[avatar_definition]) ).
fof(f1425,plain,
spl92_185,
inference(avatar_split_clause,[],[f184,f1422]) ).
fof(f1427,definition,
( spl92_186
<=> sK60 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK14)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_186])],[avatar_definition]) ).
fof(f1430,plain,
spl92_186,
inference(avatar_split_clause,[],[f185,f1427]) ).
fof(f1432,definition,
( spl92_187
<=> sK59 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK13)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_187])],[avatar_definition]) ).
fof(f1435,plain,
spl92_187,
inference(avatar_split_clause,[],[f186,f1432]) ).
fof(f1437,definition,
( spl92_188
<=> sK57 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK13)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_188])],[avatar_definition]) ).
fof(f1440,plain,
spl92_188,
inference(avatar_split_clause,[],[f187,f1437]) ).
fof(f1442,definition,
( spl92_189
<=> sK58 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK12)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_189])],[avatar_definition]) ).
fof(f1445,plain,
spl92_189,
inference(avatar_split_clause,[],[f188,f1442]) ).
fof(f1447,definition,
( spl92_190
<=> sK56 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK12)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_190])],[avatar_definition]) ).
fof(f1450,plain,
spl92_190,
inference(avatar_split_clause,[],[f189,f1447]) ).
fof(f1452,definition,
( spl92_191
<=> sK55 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK11)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_191])],[avatar_definition]) ).
fof(f1455,plain,
spl92_191,
inference(avatar_split_clause,[],[f190,f1452]) ).
fof(f1457,definition,
( spl92_192
<=> sK53 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK11)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_192])],[avatar_definition]) ).
fof(f1460,plain,
spl92_192,
inference(avatar_split_clause,[],[f191,f1457]) ).
fof(f1462,definition,
( spl92_193
<=> sK54 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK10)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_193])],[avatar_definition]) ).
fof(f1465,plain,
spl92_193,
inference(avatar_split_clause,[],[f192,f1462]) ).
fof(f1467,definition,
( spl92_194
<=> sK52 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK10)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_194])],[avatar_definition]) ).
fof(f1470,plain,
spl92_194,
inference(avatar_split_clause,[],[f193,f1467]) ).
fof(f1472,definition,
( spl92_195
<=> sK51 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK9)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_195])],[avatar_definition]) ).
fof(f1475,plain,
spl92_195,
inference(avatar_split_clause,[],[f194,f1472]) ).
fof(f1477,definition,
( spl92_196
<=> sK49 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK9)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_196])],[avatar_definition]) ).
fof(f1480,plain,
spl92_196,
inference(avatar_split_clause,[],[f195,f1477]) ).
fof(f1482,definition,
( spl92_197
<=> sK50 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK8)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_197])],[avatar_definition]) ).
fof(f1485,plain,
spl92_197,
inference(avatar_split_clause,[],[f196,f1482]) ).
fof(f1487,definition,
( spl92_198
<=> sK48 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK8)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_198])],[avatar_definition]) ).
fof(f1490,plain,
spl92_198,
inference(avatar_split_clause,[],[f197,f1487]) ).
fof(f1492,definition,
( spl92_199
<=> sK47 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK7)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_199])],[avatar_definition]) ).
fof(f1495,plain,
spl92_199,
inference(avatar_split_clause,[],[f198,f1492]) ).
fof(f1497,definition,
( spl92_200
<=> sK45 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK7)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_200])],[avatar_definition]) ).
fof(f1500,plain,
spl92_200,
inference(avatar_split_clause,[],[f199,f1497]) ).
fof(f1502,definition,
( spl92_201
<=> sK46 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK6)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_201])],[avatar_definition]) ).
fof(f1505,plain,
spl92_201,
inference(avatar_split_clause,[],[f200,f1502]) ).
fof(f1507,definition,
( spl92_202
<=> sK44 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK6)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_202])],[avatar_definition]) ).
fof(f1510,plain,
spl92_202,
inference(avatar_split_clause,[],[f201,f1507]) ).
fof(f1512,definition,
( spl92_203
<=> sK43 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK5)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_203])],[avatar_definition]) ).
fof(f1515,plain,
spl92_203,
inference(avatar_split_clause,[],[f202,f1512]) ).
fof(f1517,definition,
( spl92_204
<=> sK41 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK5)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_204])],[avatar_definition]) ).
fof(f1520,plain,
spl92_204,
inference(avatar_split_clause,[],[f203,f1517]) ).
fof(f1522,definition,
( spl92_205
<=> sK42 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK4)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_205])],[avatar_definition]) ).
fof(f1525,plain,
spl92_205,
inference(avatar_split_clause,[],[f204,f1522]) ).
fof(f1527,definition,
( spl92_206
<=> sK40 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK4)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_206])],[avatar_definition]) ).
fof(f1530,plain,
spl92_206,
inference(avatar_split_clause,[],[f205,f1527]) ).
fof(f1532,definition,
( spl92_207
<=> sK39 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK3)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_207])],[avatar_definition]) ).
fof(f1535,plain,
spl92_207,
inference(avatar_split_clause,[],[f206,f1532]) ).
fof(f1537,definition,
( spl92_208
<=> sK37 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK3)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_208])],[avatar_definition]) ).
fof(f1540,plain,
spl92_208,
inference(avatar_split_clause,[],[f207,f1537]) ).
fof(f1542,definition,
( spl92_209
<=> sK38 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK2)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_209])],[avatar_definition]) ).
fof(f1545,plain,
spl92_209,
inference(avatar_split_clause,[],[f208,f1542]) ).
fof(f1547,definition,
( spl92_210
<=> sK36 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK2)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_210])],[avatar_definition]) ).
fof(f1550,plain,
spl92_210,
inference(avatar_split_clause,[],[f209,f1547]) ).
fof(f1552,definition,
( spl92_211
<=> sK35 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK1)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_211])],[avatar_definition]) ).
fof(f1555,plain,
spl92_211,
inference(avatar_split_clause,[],[f210,f1552]) ).
fof(f1557,definition,
( spl92_212
<=> sK33 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK1)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_212])],[avatar_definition]) ).
fof(f1560,plain,
spl92_212,
inference(avatar_split_clause,[],[f211,f1557]) ).
fof(f1562,definition,
( spl92_213
<=> sK34 = succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(sK0)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_213])],[avatar_definition]) ).
fof(f1565,plain,
spl92_213,
inference(avatar_split_clause,[],[f212,f1562]) ).
fof(f1567,definition,
( spl92_214
<=> sK32 = pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(sK0)))))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl92_214])],[avatar_definition]) ).
fof(f1570,plain,
spl92_214,
inference(avatar_split_clause,[],[f213,f1567]) ).
fof(f1572,definition,
( spl92_215
<=> n15 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_215])],[avatar_definition]) ).
fof(f1576,definition,
( spl92_216
<=> n14 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_216])],[avatar_definition]) ).
fof(f1580,definition,
( spl92_217
<=> n13 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_217])],[avatar_definition]) ).
fof(f1584,definition,
( spl92_218
<=> n12 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_218])],[avatar_definition]) ).
fof(f1588,definition,
( spl92_219
<=> n11 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_219])],[avatar_definition]) ).
fof(f1592,definition,
( spl92_220
<=> n10 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_220])],[avatar_definition]) ).
fof(f1596,definition,
( spl92_221
<=> n9 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_221])],[avatar_definition]) ).
fof(f1600,definition,
( spl92_222
<=> n8 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_222])],[avatar_definition]) ).
fof(f1604,definition,
( spl92_223
<=> n7 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_223])],[avatar_definition]) ).
fof(f1608,definition,
( spl92_224
<=> n6 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_224])],[avatar_definition]) ).
fof(f1612,definition,
( spl92_225
<=> n5 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_225])],[avatar_definition]) ).
fof(f1616,definition,
( spl92_226
<=> n4 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_226])],[avatar_definition]) ).
fof(f1620,definition,
( spl92_227
<=> n3 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_227])],[avatar_definition]) ).
fof(f1624,definition,
( spl92_228
<=> n2 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_228])],[avatar_definition]) ).
fof(f1628,definition,
( spl92_229
<=> n1 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_229])],[avatar_definition]) ).
fof(f1632,definition,
( spl92_230
<=> n0 = sK1 ),
introduced(definition,[new_symbols(definition,[spl92_230])],[avatar_definition]) ).
fof(f1635,plain,
( spl92_215
| spl92_216
| spl92_217
| spl92_218
| spl92_219
| spl92_220
| spl92_221
| spl92_222
| spl92_223
| spl92_224
| spl92_225
| spl92_226
| spl92_227
| spl92_228
| spl92_229
| spl92_230 ),
inference(avatar_split_clause,[],[f214,f1632,f1628,f1624,f1620,f1616,f1612,f1608,f1604,f1600,f1596,f1592,f1588,f1584,f1580,f1576,f1572]) ).
fof(f1637,definition,
( spl92_231
<=> n15 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_231])],[avatar_definition]) ).
fof(f1641,definition,
( spl92_232
<=> n14 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_232])],[avatar_definition]) ).
fof(f1645,definition,
( spl92_233
<=> n13 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_233])],[avatar_definition]) ).
fof(f1649,definition,
( spl92_234
<=> n12 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_234])],[avatar_definition]) ).
fof(f1653,definition,
( spl92_235
<=> n11 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_235])],[avatar_definition]) ).
fof(f1657,definition,
( spl92_236
<=> n10 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_236])],[avatar_definition]) ).
fof(f1661,definition,
( spl92_237
<=> n9 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_237])],[avatar_definition]) ).
fof(f1665,definition,
( spl92_238
<=> n8 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_238])],[avatar_definition]) ).
fof(f1669,definition,
( spl92_239
<=> n7 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_239])],[avatar_definition]) ).
fof(f1673,definition,
( spl92_240
<=> n6 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_240])],[avatar_definition]) ).
fof(f1677,definition,
( spl92_241
<=> n5 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_241])],[avatar_definition]) ).
fof(f1681,definition,
( spl92_242
<=> n4 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_242])],[avatar_definition]) ).
fof(f1685,definition,
( spl92_243
<=> n3 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_243])],[avatar_definition]) ).
fof(f1689,definition,
( spl92_244
<=> n2 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_244])],[avatar_definition]) ).
fof(f1693,definition,
( spl92_245
<=> n1 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_245])],[avatar_definition]) ).
fof(f1697,definition,
( spl92_246
<=> n0 = sK0 ),
introduced(definition,[new_symbols(definition,[spl92_246])],[avatar_definition]) ).
fof(f1700,plain,
( spl92_231
| spl92_232
| spl92_233
| spl92_234
| spl92_235
| spl92_236
| spl92_237
| spl92_238
| spl92_239
| spl92_240
| spl92_241
| spl92_242
| spl92_243
| spl92_244
| spl92_245
| spl92_246 ),
inference(avatar_split_clause,[],[f215,f1697,f1693,f1689,f1685,f1681,f1677,f1673,f1669,f1665,f1661,f1657,f1653,f1649,f1645,f1641,f1637]) ).
fof(f1702,definition,
( spl92_247
<=> n14 = sum(n15,n15) ),
introduced(definition,[new_symbols(definition,[spl92_247])],[avatar_definition]) ).
fof(f1705,plain,
spl92_247,
inference(avatar_split_clause,[],[f216,f1702]) ).
fof(f1707,definition,
( spl92_248
<=> n13 = sum(n15,n14) ),
introduced(definition,[new_symbols(definition,[spl92_248])],[avatar_definition]) ).
fof(f1710,plain,
spl92_248,
inference(avatar_split_clause,[],[f217,f1707]) ).
fof(f1712,definition,
( spl92_249
<=> n12 = sum(n15,n13) ),
introduced(definition,[new_symbols(definition,[spl92_249])],[avatar_definition]) ).
fof(f1715,plain,
spl92_249,
inference(avatar_split_clause,[],[f218,f1712]) ).
fof(f1717,definition,
( spl92_250
<=> n11 = sum(n15,n12) ),
introduced(definition,[new_symbols(definition,[spl92_250])],[avatar_definition]) ).
fof(f1720,plain,
spl92_250,
inference(avatar_split_clause,[],[f219,f1717]) ).
fof(f1722,definition,
( spl92_251
<=> n10 = sum(n15,n11) ),
introduced(definition,[new_symbols(definition,[spl92_251])],[avatar_definition]) ).
fof(f1725,plain,
spl92_251,
inference(avatar_split_clause,[],[f220,f1722]) ).
fof(f1727,definition,
( spl92_252
<=> n9 = sum(n15,n10) ),
introduced(definition,[new_symbols(definition,[spl92_252])],[avatar_definition]) ).
fof(f1730,plain,
spl92_252,
inference(avatar_split_clause,[],[f221,f1727]) ).
fof(f1732,definition,
( spl92_253
<=> n8 = sum(n15,n9) ),
introduced(definition,[new_symbols(definition,[spl92_253])],[avatar_definition]) ).
fof(f1735,plain,
spl92_253,
inference(avatar_split_clause,[],[f222,f1732]) ).
fof(f1737,definition,
( spl92_254
<=> n7 = sum(n15,n8) ),
introduced(definition,[new_symbols(definition,[spl92_254])],[avatar_definition]) ).
fof(f1740,plain,
spl92_254,
inference(avatar_split_clause,[],[f223,f1737]) ).
fof(f1742,definition,
( spl92_255
<=> n6 = sum(n15,n7) ),
introduced(definition,[new_symbols(definition,[spl92_255])],[avatar_definition]) ).
fof(f1745,plain,
spl92_255,
inference(avatar_split_clause,[],[f224,f1742]) ).
fof(f1747,definition,
( spl92_256
<=> n5 = sum(n15,n6) ),
introduced(definition,[new_symbols(definition,[spl92_256])],[avatar_definition]) ).
fof(f1750,plain,
spl92_256,
inference(avatar_split_clause,[],[f225,f1747]) ).
fof(f1752,definition,
( spl92_257
<=> n4 = sum(n15,n5) ),
introduced(definition,[new_symbols(definition,[spl92_257])],[avatar_definition]) ).
fof(f1755,plain,
spl92_257,
inference(avatar_split_clause,[],[f226,f1752]) ).
fof(f1757,definition,
( spl92_258
<=> n3 = sum(n15,n4) ),
introduced(definition,[new_symbols(definition,[spl92_258])],[avatar_definition]) ).
fof(f1760,plain,
spl92_258,
inference(avatar_split_clause,[],[f227,f1757]) ).
fof(f1762,definition,
( spl92_259
<=> n2 = sum(n15,n3) ),
introduced(definition,[new_symbols(definition,[spl92_259])],[avatar_definition]) ).
fof(f1765,plain,
spl92_259,
inference(avatar_split_clause,[],[f228,f1762]) ).
fof(f1767,definition,
( spl92_260
<=> n1 = sum(n15,n2) ),
introduced(definition,[new_symbols(definition,[spl92_260])],[avatar_definition]) ).
fof(f1770,plain,
spl92_260,
inference(avatar_split_clause,[],[f229,f1767]) ).
fof(f1772,definition,
( spl92_261
<=> n0 = sum(n15,n1) ),
introduced(definition,[new_symbols(definition,[spl92_261])],[avatar_definition]) ).
fof(f1775,plain,
spl92_261,
inference(avatar_split_clause,[],[f230,f1772]) ).
fof(f1777,definition,
( spl92_262
<=> n15 = sum(n15,n0) ),
introduced(definition,[new_symbols(definition,[spl92_262])],[avatar_definition]) ).
fof(f1780,plain,
spl92_262,
inference(avatar_split_clause,[],[f231,f1777]) ).
fof(f1782,definition,
( spl92_263
<=> n13 = sum(n14,n15) ),
introduced(definition,[new_symbols(definition,[spl92_263])],[avatar_definition]) ).
fof(f1785,plain,
spl92_263,
inference(avatar_split_clause,[],[f232,f1782]) ).
fof(f1787,definition,
( spl92_264
<=> n12 = sum(n14,n14) ),
introduced(definition,[new_symbols(definition,[spl92_264])],[avatar_definition]) ).
fof(f1790,plain,
spl92_264,
inference(avatar_split_clause,[],[f233,f1787]) ).
fof(f1792,definition,
( spl92_265
<=> n11 = sum(n14,n13) ),
introduced(definition,[new_symbols(definition,[spl92_265])],[avatar_definition]) ).
fof(f1795,plain,
spl92_265,
inference(avatar_split_clause,[],[f234,f1792]) ).
fof(f1797,definition,
( spl92_266
<=> n10 = sum(n14,n12) ),
introduced(definition,[new_symbols(definition,[spl92_266])],[avatar_definition]) ).
fof(f1800,plain,
spl92_266,
inference(avatar_split_clause,[],[f235,f1797]) ).
fof(f1802,definition,
( spl92_267
<=> n9 = sum(n14,n11) ),
introduced(definition,[new_symbols(definition,[spl92_267])],[avatar_definition]) ).
fof(f1805,plain,
spl92_267,
inference(avatar_split_clause,[],[f236,f1802]) ).
fof(f1807,definition,
( spl92_268
<=> n8 = sum(n14,n10) ),
introduced(definition,[new_symbols(definition,[spl92_268])],[avatar_definition]) ).
fof(f1810,plain,
spl92_268,
inference(avatar_split_clause,[],[f237,f1807]) ).
fof(f1812,definition,
( spl92_269
<=> n7 = sum(n14,n9) ),
introduced(definition,[new_symbols(definition,[spl92_269])],[avatar_definition]) ).
fof(f1815,plain,
spl92_269,
inference(avatar_split_clause,[],[f238,f1812]) ).
fof(f1817,definition,
( spl92_270
<=> n6 = sum(n14,n8) ),
introduced(definition,[new_symbols(definition,[spl92_270])],[avatar_definition]) ).
fof(f1820,plain,
spl92_270,
inference(avatar_split_clause,[],[f239,f1817]) ).
fof(f1822,definition,
( spl92_271
<=> n5 = sum(n14,n7) ),
introduced(definition,[new_symbols(definition,[spl92_271])],[avatar_definition]) ).
fof(f1825,plain,
spl92_271,
inference(avatar_split_clause,[],[f240,f1822]) ).
fof(f1827,definition,
( spl92_272
<=> n4 = sum(n14,n6) ),
introduced(definition,[new_symbols(definition,[spl92_272])],[avatar_definition]) ).
fof(f1830,plain,
spl92_272,
inference(avatar_split_clause,[],[f241,f1827]) ).
fof(f1832,definition,
( spl92_273
<=> n3 = sum(n14,n5) ),
introduced(definition,[new_symbols(definition,[spl92_273])],[avatar_definition]) ).
fof(f1835,plain,
spl92_273,
inference(avatar_split_clause,[],[f242,f1832]) ).
fof(f1837,definition,
( spl92_274
<=> n2 = sum(n14,n4) ),
introduced(definition,[new_symbols(definition,[spl92_274])],[avatar_definition]) ).
fof(f1840,plain,
spl92_274,
inference(avatar_split_clause,[],[f243,f1837]) ).
fof(f1842,definition,
( spl92_275
<=> n1 = sum(n14,n3) ),
introduced(definition,[new_symbols(definition,[spl92_275])],[avatar_definition]) ).
fof(f1845,plain,
spl92_275,
inference(avatar_split_clause,[],[f244,f1842]) ).
fof(f1847,definition,
( spl92_276
<=> n0 = sum(n14,n2) ),
introduced(definition,[new_symbols(definition,[spl92_276])],[avatar_definition]) ).
fof(f1850,plain,
spl92_276,
inference(avatar_split_clause,[],[f245,f1847]) ).
fof(f1852,definition,
( spl92_277
<=> n15 = sum(n14,n1) ),
introduced(definition,[new_symbols(definition,[spl92_277])],[avatar_definition]) ).
fof(f1855,plain,
spl92_277,
inference(avatar_split_clause,[],[f246,f1852]) ).
fof(f1857,definition,
( spl92_278
<=> n14 = sum(n14,n0) ),
introduced(definition,[new_symbols(definition,[spl92_278])],[avatar_definition]) ).
fof(f1860,plain,
spl92_278,
inference(avatar_split_clause,[],[f247,f1857]) ).
fof(f1862,definition,
( spl92_279
<=> n12 = sum(n13,n15) ),
introduced(definition,[new_symbols(definition,[spl92_279])],[avatar_definition]) ).
fof(f1865,plain,
spl92_279,
inference(avatar_split_clause,[],[f248,f1862]) ).
fof(f1867,definition,
( spl92_280
<=> n11 = sum(n13,n14) ),
introduced(definition,[new_symbols(definition,[spl92_280])],[avatar_definition]) ).
fof(f1870,plain,
spl92_280,
inference(avatar_split_clause,[],[f249,f1867]) ).
fof(f1872,definition,
( spl92_281
<=> n10 = sum(n13,n13) ),
introduced(definition,[new_symbols(definition,[spl92_281])],[avatar_definition]) ).
fof(f1875,plain,
spl92_281,
inference(avatar_split_clause,[],[f250,f1872]) ).
fof(f1877,definition,
( spl92_282
<=> n9 = sum(n13,n12) ),
introduced(definition,[new_symbols(definition,[spl92_282])],[avatar_definition]) ).
fof(f1880,plain,
spl92_282,
inference(avatar_split_clause,[],[f251,f1877]) ).
fof(f1882,definition,
( spl92_283
<=> n8 = sum(n13,n11) ),
introduced(definition,[new_symbols(definition,[spl92_283])],[avatar_definition]) ).
fof(f1885,plain,
spl92_283,
inference(avatar_split_clause,[],[f252,f1882]) ).
fof(f1887,definition,
( spl92_284
<=> n7 = sum(n13,n10) ),
introduced(definition,[new_symbols(definition,[spl92_284])],[avatar_definition]) ).
fof(f1890,plain,
spl92_284,
inference(avatar_split_clause,[],[f253,f1887]) ).
fof(f1892,definition,
( spl92_285
<=> n6 = sum(n13,n9) ),
introduced(definition,[new_symbols(definition,[spl92_285])],[avatar_definition]) ).
fof(f1895,plain,
spl92_285,
inference(avatar_split_clause,[],[f254,f1892]) ).
fof(f1897,definition,
( spl92_286
<=> n5 = sum(n13,n8) ),
introduced(definition,[new_symbols(definition,[spl92_286])],[avatar_definition]) ).
fof(f1900,plain,
spl92_286,
inference(avatar_split_clause,[],[f255,f1897]) ).
fof(f1902,definition,
( spl92_287
<=> n4 = sum(n13,n7) ),
introduced(definition,[new_symbols(definition,[spl92_287])],[avatar_definition]) ).
fof(f1905,plain,
spl92_287,
inference(avatar_split_clause,[],[f256,f1902]) ).
fof(f1907,definition,
( spl92_288
<=> n3 = sum(n13,n6) ),
introduced(definition,[new_symbols(definition,[spl92_288])],[avatar_definition]) ).
fof(f1910,plain,
spl92_288,
inference(avatar_split_clause,[],[f257,f1907]) ).
fof(f1912,definition,
( spl92_289
<=> n2 = sum(n13,n5) ),
introduced(definition,[new_symbols(definition,[spl92_289])],[avatar_definition]) ).
fof(f1915,plain,
spl92_289,
inference(avatar_split_clause,[],[f258,f1912]) ).
fof(f1917,definition,
( spl92_290
<=> n1 = sum(n13,n4) ),
introduced(definition,[new_symbols(definition,[spl92_290])],[avatar_definition]) ).
fof(f1920,plain,
spl92_290,
inference(avatar_split_clause,[],[f259,f1917]) ).
fof(f1922,definition,
( spl92_291
<=> n0 = sum(n13,n3) ),
introduced(definition,[new_symbols(definition,[spl92_291])],[avatar_definition]) ).
fof(f1925,plain,
spl92_291,
inference(avatar_split_clause,[],[f260,f1922]) ).
fof(f1927,definition,
( spl92_292
<=> n15 = sum(n13,n2) ),
introduced(definition,[new_symbols(definition,[spl92_292])],[avatar_definition]) ).
fof(f1930,plain,
spl92_292,
inference(avatar_split_clause,[],[f261,f1927]) ).
fof(f1932,definition,
( spl92_293
<=> n14 = sum(n13,n1) ),
introduced(definition,[new_symbols(definition,[spl92_293])],[avatar_definition]) ).
fof(f1935,plain,
spl92_293,
inference(avatar_split_clause,[],[f262,f1932]) ).
fof(f1937,definition,
( spl92_294
<=> n13 = sum(n13,n0) ),
introduced(definition,[new_symbols(definition,[spl92_294])],[avatar_definition]) ).
fof(f1940,plain,
spl92_294,
inference(avatar_split_clause,[],[f263,f1937]) ).
fof(f1942,definition,
( spl92_295
<=> n11 = sum(n12,n15) ),
introduced(definition,[new_symbols(definition,[spl92_295])],[avatar_definition]) ).
fof(f1945,plain,
spl92_295,
inference(avatar_split_clause,[],[f264,f1942]) ).
fof(f1947,definition,
( spl92_296
<=> n10 = sum(n12,n14) ),
introduced(definition,[new_symbols(definition,[spl92_296])],[avatar_definition]) ).
fof(f1950,plain,
spl92_296,
inference(avatar_split_clause,[],[f265,f1947]) ).
fof(f1952,definition,
( spl92_297
<=> n9 = sum(n12,n13) ),
introduced(definition,[new_symbols(definition,[spl92_297])],[avatar_definition]) ).
fof(f1955,plain,
spl92_297,
inference(avatar_split_clause,[],[f266,f1952]) ).
fof(f1957,definition,
( spl92_298
<=> n8 = sum(n12,n12) ),
introduced(definition,[new_symbols(definition,[spl92_298])],[avatar_definition]) ).
fof(f1960,plain,
spl92_298,
inference(avatar_split_clause,[],[f267,f1957]) ).
fof(f1962,definition,
( spl92_299
<=> n7 = sum(n12,n11) ),
introduced(definition,[new_symbols(definition,[spl92_299])],[avatar_definition]) ).
fof(f1965,plain,
spl92_299,
inference(avatar_split_clause,[],[f268,f1962]) ).
fof(f1967,definition,
( spl92_300
<=> n6 = sum(n12,n10) ),
introduced(definition,[new_symbols(definition,[spl92_300])],[avatar_definition]) ).
fof(f1970,plain,
spl92_300,
inference(avatar_split_clause,[],[f269,f1967]) ).
fof(f1972,definition,
( spl92_301
<=> n5 = sum(n12,n9) ),
introduced(definition,[new_symbols(definition,[spl92_301])],[avatar_definition]) ).
fof(f1975,plain,
spl92_301,
inference(avatar_split_clause,[],[f270,f1972]) ).
fof(f1977,definition,
( spl92_302
<=> n4 = sum(n12,n8) ),
introduced(definition,[new_symbols(definition,[spl92_302])],[avatar_definition]) ).
fof(f1980,plain,
spl92_302,
inference(avatar_split_clause,[],[f271,f1977]) ).
fof(f1982,definition,
( spl92_303
<=> n3 = sum(n12,n7) ),
introduced(definition,[new_symbols(definition,[spl92_303])],[avatar_definition]) ).
fof(f1985,plain,
spl92_303,
inference(avatar_split_clause,[],[f272,f1982]) ).
fof(f1987,definition,
( spl92_304
<=> n2 = sum(n12,n6) ),
introduced(definition,[new_symbols(definition,[spl92_304])],[avatar_definition]) ).
fof(f1990,plain,
spl92_304,
inference(avatar_split_clause,[],[f273,f1987]) ).
fof(f1992,definition,
( spl92_305
<=> n1 = sum(n12,n5) ),
introduced(definition,[new_symbols(definition,[spl92_305])],[avatar_definition]) ).
fof(f1995,plain,
spl92_305,
inference(avatar_split_clause,[],[f274,f1992]) ).
fof(f1997,definition,
( spl92_306
<=> n0 = sum(n12,n4) ),
introduced(definition,[new_symbols(definition,[spl92_306])],[avatar_definition]) ).
fof(f2000,plain,
spl92_306,
inference(avatar_split_clause,[],[f275,f1997]) ).
fof(f2002,definition,
( spl92_307
<=> n15 = sum(n12,n3) ),
introduced(definition,[new_symbols(definition,[spl92_307])],[avatar_definition]) ).
fof(f2005,plain,
spl92_307,
inference(avatar_split_clause,[],[f276,f2002]) ).
fof(f2007,definition,
( spl92_308
<=> n14 = sum(n12,n2) ),
introduced(definition,[new_symbols(definition,[spl92_308])],[avatar_definition]) ).
fof(f2010,plain,
spl92_308,
inference(avatar_split_clause,[],[f277,f2007]) ).
fof(f2012,definition,
( spl92_309
<=> n13 = sum(n12,n1) ),
introduced(definition,[new_symbols(definition,[spl92_309])],[avatar_definition]) ).
fof(f2015,plain,
spl92_309,
inference(avatar_split_clause,[],[f278,f2012]) ).
fof(f2017,definition,
( spl92_310
<=> n12 = sum(n12,n0) ),
introduced(definition,[new_symbols(definition,[spl92_310])],[avatar_definition]) ).
fof(f2020,plain,
spl92_310,
inference(avatar_split_clause,[],[f279,f2017]) ).
fof(f2022,definition,
( spl92_311
<=> n10 = sum(n11,n15) ),
introduced(definition,[new_symbols(definition,[spl92_311])],[avatar_definition]) ).
fof(f2025,plain,
spl92_311,
inference(avatar_split_clause,[],[f280,f2022]) ).
fof(f2027,definition,
( spl92_312
<=> n9 = sum(n11,n14) ),
introduced(definition,[new_symbols(definition,[spl92_312])],[avatar_definition]) ).
fof(f2030,plain,
spl92_312,
inference(avatar_split_clause,[],[f281,f2027]) ).
fof(f2032,definition,
( spl92_313
<=> n8 = sum(n11,n13) ),
introduced(definition,[new_symbols(definition,[spl92_313])],[avatar_definition]) ).
fof(f2035,plain,
spl92_313,
inference(avatar_split_clause,[],[f282,f2032]) ).
fof(f2037,definition,
( spl92_314
<=> n7 = sum(n11,n12) ),
introduced(definition,[new_symbols(definition,[spl92_314])],[avatar_definition]) ).
fof(f2040,plain,
spl92_314,
inference(avatar_split_clause,[],[f283,f2037]) ).
fof(f2042,definition,
( spl92_315
<=> n6 = sum(n11,n11) ),
introduced(definition,[new_symbols(definition,[spl92_315])],[avatar_definition]) ).
fof(f2045,plain,
spl92_315,
inference(avatar_split_clause,[],[f284,f2042]) ).
fof(f2047,definition,
( spl92_316
<=> n5 = sum(n11,n10) ),
introduced(definition,[new_symbols(definition,[spl92_316])],[avatar_definition]) ).
fof(f2050,plain,
spl92_316,
inference(avatar_split_clause,[],[f285,f2047]) ).
fof(f2052,definition,
( spl92_317
<=> n4 = sum(n11,n9) ),
introduced(definition,[new_symbols(definition,[spl92_317])],[avatar_definition]) ).
fof(f2055,plain,
spl92_317,
inference(avatar_split_clause,[],[f286,f2052]) ).
fof(f2057,definition,
( spl92_318
<=> n3 = sum(n11,n8) ),
introduced(definition,[new_symbols(definition,[spl92_318])],[avatar_definition]) ).
fof(f2060,plain,
spl92_318,
inference(avatar_split_clause,[],[f287,f2057]) ).
fof(f2062,definition,
( spl92_319
<=> n2 = sum(n11,n7) ),
introduced(definition,[new_symbols(definition,[spl92_319])],[avatar_definition]) ).
fof(f2065,plain,
spl92_319,
inference(avatar_split_clause,[],[f288,f2062]) ).
fof(f2067,definition,
( spl92_320
<=> n1 = sum(n11,n6) ),
introduced(definition,[new_symbols(definition,[spl92_320])],[avatar_definition]) ).
fof(f2070,plain,
spl92_320,
inference(avatar_split_clause,[],[f289,f2067]) ).
fof(f2072,definition,
( spl92_321
<=> n0 = sum(n11,n5) ),
introduced(definition,[new_symbols(definition,[spl92_321])],[avatar_definition]) ).
fof(f2075,plain,
spl92_321,
inference(avatar_split_clause,[],[f290,f2072]) ).
fof(f2077,definition,
( spl92_322
<=> n15 = sum(n11,n4) ),
introduced(definition,[new_symbols(definition,[spl92_322])],[avatar_definition]) ).
fof(f2080,plain,
spl92_322,
inference(avatar_split_clause,[],[f291,f2077]) ).
fof(f2082,definition,
( spl92_323
<=> n14 = sum(n11,n3) ),
introduced(definition,[new_symbols(definition,[spl92_323])],[avatar_definition]) ).
fof(f2085,plain,
spl92_323,
inference(avatar_split_clause,[],[f292,f2082]) ).
fof(f2087,definition,
( spl92_324
<=> n13 = sum(n11,n2) ),
introduced(definition,[new_symbols(definition,[spl92_324])],[avatar_definition]) ).
fof(f2090,plain,
spl92_324,
inference(avatar_split_clause,[],[f293,f2087]) ).
fof(f2092,definition,
( spl92_325
<=> n12 = sum(n11,n1) ),
introduced(definition,[new_symbols(definition,[spl92_325])],[avatar_definition]) ).
fof(f2095,plain,
spl92_325,
inference(avatar_split_clause,[],[f294,f2092]) ).
fof(f2097,definition,
( spl92_326
<=> n11 = sum(n11,n0) ),
introduced(definition,[new_symbols(definition,[spl92_326])],[avatar_definition]) ).
fof(f2100,plain,
spl92_326,
inference(avatar_split_clause,[],[f295,f2097]) ).
fof(f2102,definition,
( spl92_327
<=> n9 = sum(n10,n15) ),
introduced(definition,[new_symbols(definition,[spl92_327])],[avatar_definition]) ).
fof(f2105,plain,
spl92_327,
inference(avatar_split_clause,[],[f296,f2102]) ).
fof(f2107,definition,
( spl92_328
<=> n8 = sum(n10,n14) ),
introduced(definition,[new_symbols(definition,[spl92_328])],[avatar_definition]) ).
fof(f2110,plain,
spl92_328,
inference(avatar_split_clause,[],[f297,f2107]) ).
fof(f2112,definition,
( spl92_329
<=> n7 = sum(n10,n13) ),
introduced(definition,[new_symbols(definition,[spl92_329])],[avatar_definition]) ).
fof(f2115,plain,
spl92_329,
inference(avatar_split_clause,[],[f298,f2112]) ).
fof(f2117,definition,
( spl92_330
<=> n6 = sum(n10,n12) ),
introduced(definition,[new_symbols(definition,[spl92_330])],[avatar_definition]) ).
fof(f2120,plain,
spl92_330,
inference(avatar_split_clause,[],[f299,f2117]) ).
fof(f2122,definition,
( spl92_331
<=> n5 = sum(n10,n11) ),
introduced(definition,[new_symbols(definition,[spl92_331])],[avatar_definition]) ).
fof(f2125,plain,
spl92_331,
inference(avatar_split_clause,[],[f300,f2122]) ).
fof(f2127,definition,
( spl92_332
<=> n4 = sum(n10,n10) ),
introduced(definition,[new_symbols(definition,[spl92_332])],[avatar_definition]) ).
fof(f2130,plain,
spl92_332,
inference(avatar_split_clause,[],[f301,f2127]) ).
fof(f2132,definition,
( spl92_333
<=> n3 = sum(n10,n9) ),
introduced(definition,[new_symbols(definition,[spl92_333])],[avatar_definition]) ).
fof(f2135,plain,
spl92_333,
inference(avatar_split_clause,[],[f302,f2132]) ).
fof(f2137,definition,
( spl92_334
<=> n2 = sum(n10,n8) ),
introduced(definition,[new_symbols(definition,[spl92_334])],[avatar_definition]) ).
fof(f2140,plain,
spl92_334,
inference(avatar_split_clause,[],[f303,f2137]) ).
fof(f2142,definition,
( spl92_335
<=> n1 = sum(n10,n7) ),
introduced(definition,[new_symbols(definition,[spl92_335])],[avatar_definition]) ).
fof(f2145,plain,
spl92_335,
inference(avatar_split_clause,[],[f304,f2142]) ).
fof(f2147,definition,
( spl92_336
<=> n0 = sum(n10,n6) ),
introduced(definition,[new_symbols(definition,[spl92_336])],[avatar_definition]) ).
fof(f2150,plain,
spl92_336,
inference(avatar_split_clause,[],[f305,f2147]) ).
fof(f2152,definition,
( spl92_337
<=> n15 = sum(n10,n5) ),
introduced(definition,[new_symbols(definition,[spl92_337])],[avatar_definition]) ).
fof(f2155,plain,
spl92_337,
inference(avatar_split_clause,[],[f306,f2152]) ).
fof(f2157,definition,
( spl92_338
<=> n14 = sum(n10,n4) ),
introduced(definition,[new_symbols(definition,[spl92_338])],[avatar_definition]) ).
fof(f2160,plain,
spl92_338,
inference(avatar_split_clause,[],[f307,f2157]) ).
fof(f2162,definition,
( spl92_339
<=> n13 = sum(n10,n3) ),
introduced(definition,[new_symbols(definition,[spl92_339])],[avatar_definition]) ).
fof(f2165,plain,
spl92_339,
inference(avatar_split_clause,[],[f308,f2162]) ).
fof(f2167,definition,
( spl92_340
<=> n12 = sum(n10,n2) ),
introduced(definition,[new_symbols(definition,[spl92_340])],[avatar_definition]) ).
fof(f2170,plain,
spl92_340,
inference(avatar_split_clause,[],[f309,f2167]) ).
fof(f2172,definition,
( spl92_341
<=> n11 = sum(n10,n1) ),
introduced(definition,[new_symbols(definition,[spl92_341])],[avatar_definition]) ).
fof(f2175,plain,
spl92_341,
inference(avatar_split_clause,[],[f310,f2172]) ).
fof(f2177,definition,
( spl92_342
<=> n10 = sum(n10,n0) ),
introduced(definition,[new_symbols(definition,[spl92_342])],[avatar_definition]) ).
fof(f2180,plain,
spl92_342,
inference(avatar_split_clause,[],[f311,f2177]) ).
fof(f2182,definition,
( spl92_343
<=> n8 = sum(n9,n15) ),
introduced(definition,[new_symbols(definition,[spl92_343])],[avatar_definition]) ).
fof(f2185,plain,
spl92_343,
inference(avatar_split_clause,[],[f312,f2182]) ).
fof(f2187,definition,
( spl92_344
<=> n7 = sum(n9,n14) ),
introduced(definition,[new_symbols(definition,[spl92_344])],[avatar_definition]) ).
fof(f2190,plain,
spl92_344,
inference(avatar_split_clause,[],[f313,f2187]) ).
fof(f2192,definition,
( spl92_345
<=> n6 = sum(n9,n13) ),
introduced(definition,[new_symbols(definition,[spl92_345])],[avatar_definition]) ).
fof(f2195,plain,
spl92_345,
inference(avatar_split_clause,[],[f314,f2192]) ).
fof(f2197,definition,
( spl92_346
<=> n5 = sum(n9,n12) ),
introduced(definition,[new_symbols(definition,[spl92_346])],[avatar_definition]) ).
fof(f2200,plain,
spl92_346,
inference(avatar_split_clause,[],[f315,f2197]) ).
fof(f2202,definition,
( spl92_347
<=> n4 = sum(n9,n11) ),
introduced(definition,[new_symbols(definition,[spl92_347])],[avatar_definition]) ).
fof(f2205,plain,
spl92_347,
inference(avatar_split_clause,[],[f316,f2202]) ).
fof(f2207,definition,
( spl92_348
<=> n3 = sum(n9,n10) ),
introduced(definition,[new_symbols(definition,[spl92_348])],[avatar_definition]) ).
fof(f2210,plain,
spl92_348,
inference(avatar_split_clause,[],[f317,f2207]) ).
fof(f2212,definition,
( spl92_349
<=> n2 = sum(n9,n9) ),
introduced(definition,[new_symbols(definition,[spl92_349])],[avatar_definition]) ).
fof(f2215,plain,
spl92_349,
inference(avatar_split_clause,[],[f318,f2212]) ).
fof(f2217,definition,
( spl92_350
<=> n1 = sum(n9,n8) ),
introduced(definition,[new_symbols(definition,[spl92_350])],[avatar_definition]) ).
fof(f2220,plain,
spl92_350,
inference(avatar_split_clause,[],[f319,f2217]) ).
fof(f2222,definition,
( spl92_351
<=> n0 = sum(n9,n7) ),
introduced(definition,[new_symbols(definition,[spl92_351])],[avatar_definition]) ).
fof(f2225,plain,
spl92_351,
inference(avatar_split_clause,[],[f320,f2222]) ).
fof(f2227,definition,
( spl92_352
<=> n15 = sum(n9,n6) ),
introduced(definition,[new_symbols(definition,[spl92_352])],[avatar_definition]) ).
fof(f2230,plain,
spl92_352,
inference(avatar_split_clause,[],[f321,f2227]) ).
fof(f2232,definition,
( spl92_353
<=> n14 = sum(n9,n5) ),
introduced(definition,[new_symbols(definition,[spl92_353])],[avatar_definition]) ).
fof(f2235,plain,
spl92_353,
inference(avatar_split_clause,[],[f322,f2232]) ).
fof(f2237,definition,
( spl92_354
<=> n13 = sum(n9,n4) ),
introduced(definition,[new_symbols(definition,[spl92_354])],[avatar_definition]) ).
fof(f2240,plain,
spl92_354,
inference(avatar_split_clause,[],[f323,f2237]) ).
fof(f2242,definition,
( spl92_355
<=> n12 = sum(n9,n3) ),
introduced(definition,[new_symbols(definition,[spl92_355])],[avatar_definition]) ).
fof(f2245,plain,
spl92_355,
inference(avatar_split_clause,[],[f324,f2242]) ).
fof(f2247,definition,
( spl92_356
<=> n11 = sum(n9,n2) ),
introduced(definition,[new_symbols(definition,[spl92_356])],[avatar_definition]) ).
fof(f2250,plain,
spl92_356,
inference(avatar_split_clause,[],[f325,f2247]) ).
fof(f2252,definition,
( spl92_357
<=> n10 = sum(n9,n1) ),
introduced(definition,[new_symbols(definition,[spl92_357])],[avatar_definition]) ).
fof(f2255,plain,
spl92_357,
inference(avatar_split_clause,[],[f326,f2252]) ).
fof(f2257,definition,
( spl92_358
<=> n9 = sum(n9,n0) ),
introduced(definition,[new_symbols(definition,[spl92_358])],[avatar_definition]) ).
fof(f2260,plain,
spl92_358,
inference(avatar_split_clause,[],[f327,f2257]) ).
fof(f2262,definition,
( spl92_359
<=> n7 = sum(n8,n15) ),
introduced(definition,[new_symbols(definition,[spl92_359])],[avatar_definition]) ).
fof(f2265,plain,
spl92_359,
inference(avatar_split_clause,[],[f328,f2262]) ).
fof(f2267,definition,
( spl92_360
<=> n6 = sum(n8,n14) ),
introduced(definition,[new_symbols(definition,[spl92_360])],[avatar_definition]) ).
fof(f2270,plain,
spl92_360,
inference(avatar_split_clause,[],[f329,f2267]) ).
fof(f2272,definition,
( spl92_361
<=> n5 = sum(n8,n13) ),
introduced(definition,[new_symbols(definition,[spl92_361])],[avatar_definition]) ).
fof(f2275,plain,
spl92_361,
inference(avatar_split_clause,[],[f330,f2272]) ).
fof(f2277,definition,
( spl92_362
<=> n4 = sum(n8,n12) ),
introduced(definition,[new_symbols(definition,[spl92_362])],[avatar_definition]) ).
fof(f2280,plain,
spl92_362,
inference(avatar_split_clause,[],[f331,f2277]) ).
fof(f2282,definition,
( spl92_363
<=> n3 = sum(n8,n11) ),
introduced(definition,[new_symbols(definition,[spl92_363])],[avatar_definition]) ).
fof(f2285,plain,
spl92_363,
inference(avatar_split_clause,[],[f332,f2282]) ).
fof(f2287,definition,
( spl92_364
<=> n2 = sum(n8,n10) ),
introduced(definition,[new_symbols(definition,[spl92_364])],[avatar_definition]) ).
fof(f2290,plain,
spl92_364,
inference(avatar_split_clause,[],[f333,f2287]) ).
fof(f2292,definition,
( spl92_365
<=> n1 = sum(n8,n9) ),
introduced(definition,[new_symbols(definition,[spl92_365])],[avatar_definition]) ).
fof(f2295,plain,
spl92_365,
inference(avatar_split_clause,[],[f334,f2292]) ).
fof(f2297,definition,
( spl92_366
<=> n0 = sum(n8,n8) ),
introduced(definition,[new_symbols(definition,[spl92_366])],[avatar_definition]) ).
fof(f2300,plain,
spl92_366,
inference(avatar_split_clause,[],[f335,f2297]) ).
fof(f2302,definition,
( spl92_367
<=> n15 = sum(n8,n7) ),
introduced(definition,[new_symbols(definition,[spl92_367])],[avatar_definition]) ).
fof(f2305,plain,
spl92_367,
inference(avatar_split_clause,[],[f336,f2302]) ).
fof(f2307,definition,
( spl92_368
<=> n14 = sum(n8,n6) ),
introduced(definition,[new_symbols(definition,[spl92_368])],[avatar_definition]) ).
fof(f2310,plain,
spl92_368,
inference(avatar_split_clause,[],[f337,f2307]) ).
fof(f2312,definition,
( spl92_369
<=> n13 = sum(n8,n5) ),
introduced(definition,[new_symbols(definition,[spl92_369])],[avatar_definition]) ).
fof(f2315,plain,
spl92_369,
inference(avatar_split_clause,[],[f338,f2312]) ).
fof(f2317,definition,
( spl92_370
<=> n12 = sum(n8,n4) ),
introduced(definition,[new_symbols(definition,[spl92_370])],[avatar_definition]) ).
fof(f2320,plain,
spl92_370,
inference(avatar_split_clause,[],[f339,f2317]) ).
fof(f2322,definition,
( spl92_371
<=> n11 = sum(n8,n3) ),
introduced(definition,[new_symbols(definition,[spl92_371])],[avatar_definition]) ).
fof(f2325,plain,
spl92_371,
inference(avatar_split_clause,[],[f340,f2322]) ).
fof(f2327,definition,
( spl92_372
<=> n10 = sum(n8,n2) ),
introduced(definition,[new_symbols(definition,[spl92_372])],[avatar_definition]) ).
fof(f2330,plain,
spl92_372,
inference(avatar_split_clause,[],[f341,f2327]) ).
fof(f2332,definition,
( spl92_373
<=> n9 = sum(n8,n1) ),
introduced(definition,[new_symbols(definition,[spl92_373])],[avatar_definition]) ).
fof(f2335,plain,
spl92_373,
inference(avatar_split_clause,[],[f342,f2332]) ).
fof(f2337,definition,
( spl92_374
<=> n8 = sum(n8,n0) ),
introduced(definition,[new_symbols(definition,[spl92_374])],[avatar_definition]) ).
fof(f2340,plain,
spl92_374,
inference(avatar_split_clause,[],[f343,f2337]) ).
fof(f2342,definition,
( spl92_375
<=> n6 = sum(n7,n15) ),
introduced(definition,[new_symbols(definition,[spl92_375])],[avatar_definition]) ).
fof(f2345,plain,
spl92_375,
inference(avatar_split_clause,[],[f344,f2342]) ).
fof(f2347,definition,
( spl92_376
<=> n5 = sum(n7,n14) ),
introduced(definition,[new_symbols(definition,[spl92_376])],[avatar_definition]) ).
fof(f2350,plain,
spl92_376,
inference(avatar_split_clause,[],[f345,f2347]) ).
fof(f2352,definition,
( spl92_377
<=> n4 = sum(n7,n13) ),
introduced(definition,[new_symbols(definition,[spl92_377])],[avatar_definition]) ).
fof(f2355,plain,
spl92_377,
inference(avatar_split_clause,[],[f346,f2352]) ).
fof(f2357,definition,
( spl92_378
<=> n3 = sum(n7,n12) ),
introduced(definition,[new_symbols(definition,[spl92_378])],[avatar_definition]) ).
fof(f2360,plain,
spl92_378,
inference(avatar_split_clause,[],[f347,f2357]) ).
fof(f2362,definition,
( spl92_379
<=> n2 = sum(n7,n11) ),
introduced(definition,[new_symbols(definition,[spl92_379])],[avatar_definition]) ).
fof(f2365,plain,
spl92_379,
inference(avatar_split_clause,[],[f348,f2362]) ).
fof(f2367,definition,
( spl92_380
<=> n1 = sum(n7,n10) ),
introduced(definition,[new_symbols(definition,[spl92_380])],[avatar_definition]) ).
fof(f2370,plain,
spl92_380,
inference(avatar_split_clause,[],[f349,f2367]) ).
fof(f2372,definition,
( spl92_381
<=> n0 = sum(n7,n9) ),
introduced(definition,[new_symbols(definition,[spl92_381])],[avatar_definition]) ).
fof(f2375,plain,
spl92_381,
inference(avatar_split_clause,[],[f350,f2372]) ).
fof(f2377,definition,
( spl92_382
<=> n15 = sum(n7,n8) ),
introduced(definition,[new_symbols(definition,[spl92_382])],[avatar_definition]) ).
fof(f2380,plain,
spl92_382,
inference(avatar_split_clause,[],[f351,f2377]) ).
fof(f2382,definition,
( spl92_383
<=> n14 = sum(n7,n7) ),
introduced(definition,[new_symbols(definition,[spl92_383])],[avatar_definition]) ).
fof(f2385,plain,
spl92_383,
inference(avatar_split_clause,[],[f352,f2382]) ).
fof(f2387,definition,
( spl92_384
<=> n13 = sum(n7,n6) ),
introduced(definition,[new_symbols(definition,[spl92_384])],[avatar_definition]) ).
fof(f2390,plain,
spl92_384,
inference(avatar_split_clause,[],[f353,f2387]) ).
fof(f2392,definition,
( spl92_385
<=> n12 = sum(n7,n5) ),
introduced(definition,[new_symbols(definition,[spl92_385])],[avatar_definition]) ).
fof(f2395,plain,
spl92_385,
inference(avatar_split_clause,[],[f354,f2392]) ).
fof(f2397,definition,
( spl92_386
<=> n11 = sum(n7,n4) ),
introduced(definition,[new_symbols(definition,[spl92_386])],[avatar_definition]) ).
fof(f2400,plain,
spl92_386,
inference(avatar_split_clause,[],[f355,f2397]) ).
fof(f2402,definition,
( spl92_387
<=> n10 = sum(n7,n3) ),
introduced(definition,[new_symbols(definition,[spl92_387])],[avatar_definition]) ).
fof(f2405,plain,
spl92_387,
inference(avatar_split_clause,[],[f356,f2402]) ).
fof(f2407,definition,
( spl92_388
<=> n9 = sum(n7,n2) ),
introduced(definition,[new_symbols(definition,[spl92_388])],[avatar_definition]) ).
fof(f2410,plain,
spl92_388,
inference(avatar_split_clause,[],[f357,f2407]) ).
fof(f2412,definition,
( spl92_389
<=> n8 = sum(n7,n1) ),
introduced(definition,[new_symbols(definition,[spl92_389])],[avatar_definition]) ).
fof(f2415,plain,
spl92_389,
inference(avatar_split_clause,[],[f358,f2412]) ).
fof(f2417,definition,
( spl92_390
<=> n7 = sum(n7,n0) ),
introduced(definition,[new_symbols(definition,[spl92_390])],[avatar_definition]) ).
fof(f2420,plain,
spl92_390,
inference(avatar_split_clause,[],[f359,f2417]) ).
fof(f2422,definition,
( spl92_391
<=> n5 = sum(n6,n15) ),
introduced(definition,[new_symbols(definition,[spl92_391])],[avatar_definition]) ).
fof(f2425,plain,
spl92_391,
inference(avatar_split_clause,[],[f360,f2422]) ).
fof(f2427,definition,
( spl92_392
<=> n4 = sum(n6,n14) ),
introduced(definition,[new_symbols(definition,[spl92_392])],[avatar_definition]) ).
fof(f2430,plain,
spl92_392,
inference(avatar_split_clause,[],[f361,f2427]) ).
fof(f2432,definition,
( spl92_393
<=> n3 = sum(n6,n13) ),
introduced(definition,[new_symbols(definition,[spl92_393])],[avatar_definition]) ).
fof(f2435,plain,
spl92_393,
inference(avatar_split_clause,[],[f362,f2432]) ).
fof(f2437,definition,
( spl92_394
<=> n2 = sum(n6,n12) ),
introduced(definition,[new_symbols(definition,[spl92_394])],[avatar_definition]) ).
fof(f2440,plain,
spl92_394,
inference(avatar_split_clause,[],[f363,f2437]) ).
fof(f2442,definition,
( spl92_395
<=> n1 = sum(n6,n11) ),
introduced(definition,[new_symbols(definition,[spl92_395])],[avatar_definition]) ).
fof(f2445,plain,
spl92_395,
inference(avatar_split_clause,[],[f364,f2442]) ).
fof(f2447,definition,
( spl92_396
<=> n0 = sum(n6,n10) ),
introduced(definition,[new_symbols(definition,[spl92_396])],[avatar_definition]) ).
fof(f2450,plain,
spl92_396,
inference(avatar_split_clause,[],[f365,f2447]) ).
fof(f2452,definition,
( spl92_397
<=> n15 = sum(n6,n9) ),
introduced(definition,[new_symbols(definition,[spl92_397])],[avatar_definition]) ).
fof(f2455,plain,
spl92_397,
inference(avatar_split_clause,[],[f366,f2452]) ).
fof(f2457,definition,
( spl92_398
<=> n14 = sum(n6,n8) ),
introduced(definition,[new_symbols(definition,[spl92_398])],[avatar_definition]) ).
fof(f2460,plain,
spl92_398,
inference(avatar_split_clause,[],[f367,f2457]) ).
fof(f2462,definition,
( spl92_399
<=> n13 = sum(n6,n7) ),
introduced(definition,[new_symbols(definition,[spl92_399])],[avatar_definition]) ).
fof(f2465,plain,
spl92_399,
inference(avatar_split_clause,[],[f368,f2462]) ).
fof(f2467,definition,
( spl92_400
<=> n12 = sum(n6,n6) ),
introduced(definition,[new_symbols(definition,[spl92_400])],[avatar_definition]) ).
fof(f2470,plain,
spl92_400,
inference(avatar_split_clause,[],[f369,f2467]) ).
fof(f2472,definition,
( spl92_401
<=> n11 = sum(n6,n5) ),
introduced(definition,[new_symbols(definition,[spl92_401])],[avatar_definition]) ).
fof(f2475,plain,
spl92_401,
inference(avatar_split_clause,[],[f370,f2472]) ).
fof(f2477,definition,
( spl92_402
<=> n10 = sum(n6,n4) ),
introduced(definition,[new_symbols(definition,[spl92_402])],[avatar_definition]) ).
fof(f2480,plain,
spl92_402,
inference(avatar_split_clause,[],[f371,f2477]) ).
fof(f2482,definition,
( spl92_403
<=> n9 = sum(n6,n3) ),
introduced(definition,[new_symbols(definition,[spl92_403])],[avatar_definition]) ).
fof(f2485,plain,
spl92_403,
inference(avatar_split_clause,[],[f372,f2482]) ).
fof(f2487,definition,
( spl92_404
<=> n8 = sum(n6,n2) ),
introduced(definition,[new_symbols(definition,[spl92_404])],[avatar_definition]) ).
fof(f2490,plain,
spl92_404,
inference(avatar_split_clause,[],[f373,f2487]) ).
fof(f2492,definition,
( spl92_405
<=> n7 = sum(n6,n1) ),
introduced(definition,[new_symbols(definition,[spl92_405])],[avatar_definition]) ).
fof(f2495,plain,
spl92_405,
inference(avatar_split_clause,[],[f374,f2492]) ).
fof(f2497,definition,
( spl92_406
<=> n6 = sum(n6,n0) ),
introduced(definition,[new_symbols(definition,[spl92_406])],[avatar_definition]) ).
fof(f2500,plain,
spl92_406,
inference(avatar_split_clause,[],[f375,f2497]) ).
fof(f2502,definition,
( spl92_407
<=> n4 = sum(n5,n15) ),
introduced(definition,[new_symbols(definition,[spl92_407])],[avatar_definition]) ).
fof(f2505,plain,
spl92_407,
inference(avatar_split_clause,[],[f376,f2502]) ).
fof(f2507,definition,
( spl92_408
<=> n3 = sum(n5,n14) ),
introduced(definition,[new_symbols(definition,[spl92_408])],[avatar_definition]) ).
fof(f2510,plain,
spl92_408,
inference(avatar_split_clause,[],[f377,f2507]) ).
fof(f2512,definition,
( spl92_409
<=> n2 = sum(n5,n13) ),
introduced(definition,[new_symbols(definition,[spl92_409])],[avatar_definition]) ).
fof(f2515,plain,
spl92_409,
inference(avatar_split_clause,[],[f378,f2512]) ).
fof(f2517,definition,
( spl92_410
<=> n1 = sum(n5,n12) ),
introduced(definition,[new_symbols(definition,[spl92_410])],[avatar_definition]) ).
fof(f2520,plain,
spl92_410,
inference(avatar_split_clause,[],[f379,f2517]) ).
fof(f2522,definition,
( spl92_411
<=> n0 = sum(n5,n11) ),
introduced(definition,[new_symbols(definition,[spl92_411])],[avatar_definition]) ).
fof(f2525,plain,
spl92_411,
inference(avatar_split_clause,[],[f380,f2522]) ).
fof(f2527,definition,
( spl92_412
<=> n15 = sum(n5,n10) ),
introduced(definition,[new_symbols(definition,[spl92_412])],[avatar_definition]) ).
fof(f2530,plain,
spl92_412,
inference(avatar_split_clause,[],[f381,f2527]) ).
fof(f2532,definition,
( spl92_413
<=> n14 = sum(n5,n9) ),
introduced(definition,[new_symbols(definition,[spl92_413])],[avatar_definition]) ).
fof(f2535,plain,
spl92_413,
inference(avatar_split_clause,[],[f382,f2532]) ).
fof(f2537,definition,
( spl92_414
<=> n13 = sum(n5,n8) ),
introduced(definition,[new_symbols(definition,[spl92_414])],[avatar_definition]) ).
fof(f2540,plain,
spl92_414,
inference(avatar_split_clause,[],[f383,f2537]) ).
fof(f2542,definition,
( spl92_415
<=> n12 = sum(n5,n7) ),
introduced(definition,[new_symbols(definition,[spl92_415])],[avatar_definition]) ).
fof(f2545,plain,
spl92_415,
inference(avatar_split_clause,[],[f384,f2542]) ).
fof(f2547,definition,
( spl92_416
<=> n11 = sum(n5,n6) ),
introduced(definition,[new_symbols(definition,[spl92_416])],[avatar_definition]) ).
fof(f2550,plain,
spl92_416,
inference(avatar_split_clause,[],[f385,f2547]) ).
fof(f2552,definition,
( spl92_417
<=> n10 = sum(n5,n5) ),
introduced(definition,[new_symbols(definition,[spl92_417])],[avatar_definition]) ).
fof(f2555,plain,
spl92_417,
inference(avatar_split_clause,[],[f386,f2552]) ).
fof(f2557,definition,
( spl92_418
<=> n9 = sum(n5,n4) ),
introduced(definition,[new_symbols(definition,[spl92_418])],[avatar_definition]) ).
fof(f2560,plain,
spl92_418,
inference(avatar_split_clause,[],[f387,f2557]) ).
fof(f2562,definition,
( spl92_419
<=> n8 = sum(n5,n3) ),
introduced(definition,[new_symbols(definition,[spl92_419])],[avatar_definition]) ).
fof(f2565,plain,
spl92_419,
inference(avatar_split_clause,[],[f388,f2562]) ).
fof(f2567,definition,
( spl92_420
<=> n7 = sum(n5,n2) ),
introduced(definition,[new_symbols(definition,[spl92_420])],[avatar_definition]) ).
fof(f2570,plain,
spl92_420,
inference(avatar_split_clause,[],[f389,f2567]) ).
fof(f2572,definition,
( spl92_421
<=> n6 = sum(n5,n1) ),
introduced(definition,[new_symbols(definition,[spl92_421])],[avatar_definition]) ).
fof(f2575,plain,
spl92_421,
inference(avatar_split_clause,[],[f390,f2572]) ).
fof(f2577,definition,
( spl92_422
<=> n5 = sum(n5,n0) ),
introduced(definition,[new_symbols(definition,[spl92_422])],[avatar_definition]) ).
fof(f2580,plain,
spl92_422,
inference(avatar_split_clause,[],[f391,f2577]) ).
fof(f2582,definition,
( spl92_423
<=> n3 = sum(n4,n15) ),
introduced(definition,[new_symbols(definition,[spl92_423])],[avatar_definition]) ).
fof(f2585,plain,
spl92_423,
inference(avatar_split_clause,[],[f392,f2582]) ).
fof(f2587,definition,
( spl92_424
<=> n2 = sum(n4,n14) ),
introduced(definition,[new_symbols(definition,[spl92_424])],[avatar_definition]) ).
fof(f2590,plain,
spl92_424,
inference(avatar_split_clause,[],[f393,f2587]) ).
fof(f2592,definition,
( spl92_425
<=> n1 = sum(n4,n13) ),
introduced(definition,[new_symbols(definition,[spl92_425])],[avatar_definition]) ).
fof(f2595,plain,
spl92_425,
inference(avatar_split_clause,[],[f394,f2592]) ).
fof(f2597,definition,
( spl92_426
<=> n0 = sum(n4,n12) ),
introduced(definition,[new_symbols(definition,[spl92_426])],[avatar_definition]) ).
fof(f2600,plain,
spl92_426,
inference(avatar_split_clause,[],[f395,f2597]) ).
fof(f2602,definition,
( spl92_427
<=> n15 = sum(n4,n11) ),
introduced(definition,[new_symbols(definition,[spl92_427])],[avatar_definition]) ).
fof(f2605,plain,
spl92_427,
inference(avatar_split_clause,[],[f396,f2602]) ).
fof(f2607,definition,
( spl92_428
<=> n14 = sum(n4,n10) ),
introduced(definition,[new_symbols(definition,[spl92_428])],[avatar_definition]) ).
fof(f2610,plain,
spl92_428,
inference(avatar_split_clause,[],[f397,f2607]) ).
fof(f2612,definition,
( spl92_429
<=> n13 = sum(n4,n9) ),
introduced(definition,[new_symbols(definition,[spl92_429])],[avatar_definition]) ).
fof(f2615,plain,
spl92_429,
inference(avatar_split_clause,[],[f398,f2612]) ).
fof(f2617,definition,
( spl92_430
<=> n12 = sum(n4,n8) ),
introduced(definition,[new_symbols(definition,[spl92_430])],[avatar_definition]) ).
fof(f2620,plain,
spl92_430,
inference(avatar_split_clause,[],[f399,f2617]) ).
fof(f2622,definition,
( spl92_431
<=> n11 = sum(n4,n7) ),
introduced(definition,[new_symbols(definition,[spl92_431])],[avatar_definition]) ).
fof(f2625,plain,
spl92_431,
inference(avatar_split_clause,[],[f400,f2622]) ).
fof(f2627,definition,
( spl92_432
<=> n10 = sum(n4,n6) ),
introduced(definition,[new_symbols(definition,[spl92_432])],[avatar_definition]) ).
fof(f2630,plain,
spl92_432,
inference(avatar_split_clause,[],[f401,f2627]) ).
fof(f2632,definition,
( spl92_433
<=> n9 = sum(n4,n5) ),
introduced(definition,[new_symbols(definition,[spl92_433])],[avatar_definition]) ).
fof(f2635,plain,
spl92_433,
inference(avatar_split_clause,[],[f402,f2632]) ).
fof(f2637,definition,
( spl92_434
<=> n8 = sum(n4,n4) ),
introduced(definition,[new_symbols(definition,[spl92_434])],[avatar_definition]) ).
fof(f2640,plain,
spl92_434,
inference(avatar_split_clause,[],[f403,f2637]) ).
fof(f2642,definition,
( spl92_435
<=> n7 = sum(n4,n3) ),
introduced(definition,[new_symbols(definition,[spl92_435])],[avatar_definition]) ).
fof(f2645,plain,
spl92_435,
inference(avatar_split_clause,[],[f404,f2642]) ).
fof(f2647,definition,
( spl92_436
<=> n6 = sum(n4,n2) ),
introduced(definition,[new_symbols(definition,[spl92_436])],[avatar_definition]) ).
fof(f2650,plain,
spl92_436,
inference(avatar_split_clause,[],[f405,f2647]) ).
fof(f2652,definition,
( spl92_437
<=> n5 = sum(n4,n1) ),
introduced(definition,[new_symbols(definition,[spl92_437])],[avatar_definition]) ).
fof(f2655,plain,
spl92_437,
inference(avatar_split_clause,[],[f406,f2652]) ).
fof(f2657,definition,
( spl92_438
<=> n4 = sum(n4,n0) ),
introduced(definition,[new_symbols(definition,[spl92_438])],[avatar_definition]) ).
fof(f2660,plain,
spl92_438,
inference(avatar_split_clause,[],[f407,f2657]) ).
fof(f2662,definition,
( spl92_439
<=> n2 = sum(n3,n15) ),
introduced(definition,[new_symbols(definition,[spl92_439])],[avatar_definition]) ).
fof(f2665,plain,
spl92_439,
inference(avatar_split_clause,[],[f408,f2662]) ).
fof(f2667,definition,
( spl92_440
<=> n1 = sum(n3,n14) ),
introduced(definition,[new_symbols(definition,[spl92_440])],[avatar_definition]) ).
fof(f2670,plain,
spl92_440,
inference(avatar_split_clause,[],[f409,f2667]) ).
fof(f2672,definition,
( spl92_441
<=> n0 = sum(n3,n13) ),
introduced(definition,[new_symbols(definition,[spl92_441])],[avatar_definition]) ).
fof(f2675,plain,
spl92_441,
inference(avatar_split_clause,[],[f410,f2672]) ).
fof(f2677,definition,
( spl92_442
<=> n15 = sum(n3,n12) ),
introduced(definition,[new_symbols(definition,[spl92_442])],[avatar_definition]) ).
fof(f2680,plain,
spl92_442,
inference(avatar_split_clause,[],[f411,f2677]) ).
fof(f2682,definition,
( spl92_443
<=> n14 = sum(n3,n11) ),
introduced(definition,[new_symbols(definition,[spl92_443])],[avatar_definition]) ).
fof(f2685,plain,
spl92_443,
inference(avatar_split_clause,[],[f412,f2682]) ).
fof(f2687,definition,
( spl92_444
<=> n13 = sum(n3,n10) ),
introduced(definition,[new_symbols(definition,[spl92_444])],[avatar_definition]) ).
fof(f2690,plain,
spl92_444,
inference(avatar_split_clause,[],[f413,f2687]) ).
fof(f2692,definition,
( spl92_445
<=> n12 = sum(n3,n9) ),
introduced(definition,[new_symbols(definition,[spl92_445])],[avatar_definition]) ).
fof(f2695,plain,
spl92_445,
inference(avatar_split_clause,[],[f414,f2692]) ).
fof(f2697,definition,
( spl92_446
<=> n11 = sum(n3,n8) ),
introduced(definition,[new_symbols(definition,[spl92_446])],[avatar_definition]) ).
fof(f2700,plain,
spl92_446,
inference(avatar_split_clause,[],[f415,f2697]) ).
fof(f2702,definition,
( spl92_447
<=> n10 = sum(n3,n7) ),
introduced(definition,[new_symbols(definition,[spl92_447])],[avatar_definition]) ).
fof(f2705,plain,
spl92_447,
inference(avatar_split_clause,[],[f416,f2702]) ).
fof(f2707,definition,
( spl92_448
<=> n9 = sum(n3,n6) ),
introduced(definition,[new_symbols(definition,[spl92_448])],[avatar_definition]) ).
fof(f2710,plain,
spl92_448,
inference(avatar_split_clause,[],[f417,f2707]) ).
fof(f2712,definition,
( spl92_449
<=> n8 = sum(n3,n5) ),
introduced(definition,[new_symbols(definition,[spl92_449])],[avatar_definition]) ).
fof(f2715,plain,
spl92_449,
inference(avatar_split_clause,[],[f418,f2712]) ).
fof(f2717,definition,
( spl92_450
<=> n7 = sum(n3,n4) ),
introduced(definition,[new_symbols(definition,[spl92_450])],[avatar_definition]) ).
fof(f2720,plain,
spl92_450,
inference(avatar_split_clause,[],[f419,f2717]) ).
fof(f2722,definition,
( spl92_451
<=> n6 = sum(n3,n3) ),
introduced(definition,[new_symbols(definition,[spl92_451])],[avatar_definition]) ).
fof(f2725,plain,
spl92_451,
inference(avatar_split_clause,[],[f420,f2722]) ).
fof(f2727,definition,
( spl92_452
<=> n5 = sum(n3,n2) ),
introduced(definition,[new_symbols(definition,[spl92_452])],[avatar_definition]) ).
fof(f2730,plain,
spl92_452,
inference(avatar_split_clause,[],[f421,f2727]) ).
fof(f2732,definition,
( spl92_453
<=> n4 = sum(n3,n1) ),
introduced(definition,[new_symbols(definition,[spl92_453])],[avatar_definition]) ).
fof(f2735,plain,
spl92_453,
inference(avatar_split_clause,[],[f422,f2732]) ).
fof(f2737,definition,
( spl92_454
<=> n3 = sum(n3,n0) ),
introduced(definition,[new_symbols(definition,[spl92_454])],[avatar_definition]) ).
fof(f2740,plain,
spl92_454,
inference(avatar_split_clause,[],[f423,f2737]) ).
fof(f2742,definition,
( spl92_455
<=> n1 = sum(n2,n15) ),
introduced(definition,[new_symbols(definition,[spl92_455])],[avatar_definition]) ).
fof(f2745,plain,
spl92_455,
inference(avatar_split_clause,[],[f424,f2742]) ).
fof(f2747,definition,
( spl92_456
<=> n0 = sum(n2,n14) ),
introduced(definition,[new_symbols(definition,[spl92_456])],[avatar_definition]) ).
fof(f2750,plain,
spl92_456,
inference(avatar_split_clause,[],[f425,f2747]) ).
fof(f2752,definition,
( spl92_457
<=> n15 = sum(n2,n13) ),
introduced(definition,[new_symbols(definition,[spl92_457])],[avatar_definition]) ).
fof(f2755,plain,
spl92_457,
inference(avatar_split_clause,[],[f426,f2752]) ).
fof(f2757,definition,
( spl92_458
<=> n14 = sum(n2,n12) ),
introduced(definition,[new_symbols(definition,[spl92_458])],[avatar_definition]) ).
fof(f2760,plain,
spl92_458,
inference(avatar_split_clause,[],[f427,f2757]) ).
fof(f2762,definition,
( spl92_459
<=> n13 = sum(n2,n11) ),
introduced(definition,[new_symbols(definition,[spl92_459])],[avatar_definition]) ).
fof(f2765,plain,
spl92_459,
inference(avatar_split_clause,[],[f428,f2762]) ).
fof(f2767,definition,
( spl92_460
<=> n12 = sum(n2,n10) ),
introduced(definition,[new_symbols(definition,[spl92_460])],[avatar_definition]) ).
fof(f2770,plain,
spl92_460,
inference(avatar_split_clause,[],[f429,f2767]) ).
fof(f2772,definition,
( spl92_461
<=> n11 = sum(n2,n9) ),
introduced(definition,[new_symbols(definition,[spl92_461])],[avatar_definition]) ).
fof(f2775,plain,
spl92_461,
inference(avatar_split_clause,[],[f430,f2772]) ).
fof(f2777,definition,
( spl92_462
<=> n10 = sum(n2,n8) ),
introduced(definition,[new_symbols(definition,[spl92_462])],[avatar_definition]) ).
fof(f2780,plain,
spl92_462,
inference(avatar_split_clause,[],[f431,f2777]) ).
fof(f2782,definition,
( spl92_463
<=> n9 = sum(n2,n7) ),
introduced(definition,[new_symbols(definition,[spl92_463])],[avatar_definition]) ).
fof(f2785,plain,
spl92_463,
inference(avatar_split_clause,[],[f432,f2782]) ).
fof(f2787,definition,
( spl92_464
<=> n8 = sum(n2,n6) ),
introduced(definition,[new_symbols(definition,[spl92_464])],[avatar_definition]) ).
fof(f2790,plain,
spl92_464,
inference(avatar_split_clause,[],[f433,f2787]) ).
fof(f2792,definition,
( spl92_465
<=> n7 = sum(n2,n5) ),
introduced(definition,[new_symbols(definition,[spl92_465])],[avatar_definition]) ).
fof(f2795,plain,
spl92_465,
inference(avatar_split_clause,[],[f434,f2792]) ).
fof(f2797,definition,
( spl92_466
<=> n6 = sum(n2,n4) ),
introduced(definition,[new_symbols(definition,[spl92_466])],[avatar_definition]) ).
fof(f2800,plain,
spl92_466,
inference(avatar_split_clause,[],[f435,f2797]) ).
fof(f2802,definition,
( spl92_467
<=> n5 = sum(n2,n3) ),
introduced(definition,[new_symbols(definition,[spl92_467])],[avatar_definition]) ).
fof(f2805,plain,
spl92_467,
inference(avatar_split_clause,[],[f436,f2802]) ).
fof(f2807,definition,
( spl92_468
<=> n4 = sum(n2,n2) ),
introduced(definition,[new_symbols(definition,[spl92_468])],[avatar_definition]) ).
fof(f2810,plain,
spl92_468,
inference(avatar_split_clause,[],[f437,f2807]) ).
fof(f2812,definition,
( spl92_469
<=> n3 = sum(n2,n1) ),
introduced(definition,[new_symbols(definition,[spl92_469])],[avatar_definition]) ).
fof(f2815,plain,
spl92_469,
inference(avatar_split_clause,[],[f438,f2812]) ).
fof(f2817,definition,
( spl92_470
<=> n2 = sum(n2,n0) ),
introduced(definition,[new_symbols(definition,[spl92_470])],[avatar_definition]) ).
fof(f2820,plain,
spl92_470,
inference(avatar_split_clause,[],[f439,f2817]) ).
fof(f2822,definition,
( spl92_471
<=> n0 = sum(n1,n15) ),
introduced(definition,[new_symbols(definition,[spl92_471])],[avatar_definition]) ).
fof(f2825,plain,
spl92_471,
inference(avatar_split_clause,[],[f440,f2822]) ).
fof(f2827,definition,
( spl92_472
<=> n15 = sum(n1,n14) ),
introduced(definition,[new_symbols(definition,[spl92_472])],[avatar_definition]) ).
fof(f2830,plain,
spl92_472,
inference(avatar_split_clause,[],[f441,f2827]) ).
fof(f2832,definition,
( spl92_473
<=> n14 = sum(n1,n13) ),
introduced(definition,[new_symbols(definition,[spl92_473])],[avatar_definition]) ).
fof(f2835,plain,
spl92_473,
inference(avatar_split_clause,[],[f442,f2832]) ).
fof(f2837,definition,
( spl92_474
<=> n13 = sum(n1,n12) ),
introduced(definition,[new_symbols(definition,[spl92_474])],[avatar_definition]) ).
fof(f2840,plain,
spl92_474,
inference(avatar_split_clause,[],[f443,f2837]) ).
fof(f2842,definition,
( spl92_475
<=> n12 = sum(n1,n11) ),
introduced(definition,[new_symbols(definition,[spl92_475])],[avatar_definition]) ).
fof(f2845,plain,
spl92_475,
inference(avatar_split_clause,[],[f444,f2842]) ).
fof(f2847,definition,
( spl92_476
<=> n11 = sum(n1,n10) ),
introduced(definition,[new_symbols(definition,[spl92_476])],[avatar_definition]) ).
fof(f2850,plain,
spl92_476,
inference(avatar_split_clause,[],[f445,f2847]) ).
fof(f2852,definition,
( spl92_477
<=> n10 = sum(n1,n9) ),
introduced(definition,[new_symbols(definition,[spl92_477])],[avatar_definition]) ).
fof(f2855,plain,
spl92_477,
inference(avatar_split_clause,[],[f446,f2852]) ).
fof(f2857,definition,
( spl92_478
<=> n9 = sum(n1,n8) ),
introduced(definition,[new_symbols(definition,[spl92_478])],[avatar_definition]) ).
fof(f2860,plain,
spl92_478,
inference(avatar_split_clause,[],[f447,f2857]) ).
fof(f2862,definition,
( spl92_479
<=> n8 = sum(n1,n7) ),
introduced(definition,[new_symbols(definition,[spl92_479])],[avatar_definition]) ).
fof(f2865,plain,
spl92_479,
inference(avatar_split_clause,[],[f448,f2862]) ).
fof(f2867,definition,
( spl92_480
<=> n7 = sum(n1,n6) ),
introduced(definition,[new_symbols(definition,[spl92_480])],[avatar_definition]) ).
fof(f2870,plain,
spl92_480,
inference(avatar_split_clause,[],[f449,f2867]) ).
fof(f2872,definition,
( spl92_481
<=> n6 = sum(n1,n5) ),
introduced(definition,[new_symbols(definition,[spl92_481])],[avatar_definition]) ).
fof(f2875,plain,
spl92_481,
inference(avatar_split_clause,[],[f450,f2872]) ).
fof(f2877,definition,
( spl92_482
<=> n5 = sum(n1,n4) ),
introduced(definition,[new_symbols(definition,[spl92_482])],[avatar_definition]) ).
fof(f2880,plain,
spl92_482,
inference(avatar_split_clause,[],[f451,f2877]) ).
fof(f2882,definition,
( spl92_483
<=> n4 = sum(n1,n3) ),
introduced(definition,[new_symbols(definition,[spl92_483])],[avatar_definition]) ).
fof(f2885,plain,
spl92_483,
inference(avatar_split_clause,[],[f452,f2882]) ).
fof(f2887,definition,
( spl92_484
<=> n3 = sum(n1,n2) ),
introduced(definition,[new_symbols(definition,[spl92_484])],[avatar_definition]) ).
fof(f2890,plain,
spl92_484,
inference(avatar_split_clause,[],[f453,f2887]) ).
fof(f2892,definition,
( spl92_485
<=> n2 = sum(n1,n1) ),
introduced(definition,[new_symbols(definition,[spl92_485])],[avatar_definition]) ).
fof(f2895,plain,
spl92_485,
inference(avatar_split_clause,[],[f454,f2892]) ).
fof(f2897,definition,
( spl92_486
<=> n1 = sum(n1,n0) ),
introduced(definition,[new_symbols(definition,[spl92_486])],[avatar_definition]) ).
fof(f2900,plain,
spl92_486,
inference(avatar_split_clause,[],[f455,f2897]) ).
fof(f2902,definition,
( spl92_487
<=> n15 = sum(n0,n15) ),
introduced(definition,[new_symbols(definition,[spl92_487])],[avatar_definition]) ).
fof(f2905,plain,
spl92_487,
inference(avatar_split_clause,[],[f456,f2902]) ).
fof(f2907,definition,
( spl92_488
<=> n14 = sum(n0,n14) ),
introduced(definition,[new_symbols(definition,[spl92_488])],[avatar_definition]) ).
fof(f2910,plain,
spl92_488,
inference(avatar_split_clause,[],[f457,f2907]) ).
fof(f2912,definition,
( spl92_489
<=> n13 = sum(n0,n13) ),
introduced(definition,[new_symbols(definition,[spl92_489])],[avatar_definition]) ).
fof(f2915,plain,
spl92_489,
inference(avatar_split_clause,[],[f458,f2912]) ).
fof(f2917,definition,
( spl92_490
<=> n12 = sum(n0,n12) ),
introduced(definition,[new_symbols(definition,[spl92_490])],[avatar_definition]) ).
fof(f2920,plain,
spl92_490,
inference(avatar_split_clause,[],[f459,f2917]) ).
fof(f2922,definition,
( spl92_491
<=> n11 = sum(n0,n11) ),
introduced(definition,[new_symbols(definition,[spl92_491])],[avatar_definition]) ).
fof(f2925,plain,
spl92_491,
inference(avatar_split_clause,[],[f460,f2922]) ).
fof(f2927,definition,
( spl92_492
<=> n10 = sum(n0,n10) ),
introduced(definition,[new_symbols(definition,[spl92_492])],[avatar_definition]) ).
fof(f2930,plain,
spl92_492,
inference(avatar_split_clause,[],[f461,f2927]) ).
fof(f2932,definition,
( spl92_493
<=> n9 = sum(n0,n9) ),
introduced(definition,[new_symbols(definition,[spl92_493])],[avatar_definition]) ).
fof(f2935,plain,
spl92_493,
inference(avatar_split_clause,[],[f462,f2932]) ).
fof(f2937,definition,
( spl92_494
<=> n8 = sum(n0,n8) ),
introduced(definition,[new_symbols(definition,[spl92_494])],[avatar_definition]) ).
fof(f2940,plain,
spl92_494,
inference(avatar_split_clause,[],[f463,f2937]) ).
fof(f2942,definition,
( spl92_495
<=> n7 = sum(n0,n7) ),
introduced(definition,[new_symbols(definition,[spl92_495])],[avatar_definition]) ).
fof(f2945,plain,
spl92_495,
inference(avatar_split_clause,[],[f464,f2942]) ).
fof(f2947,definition,
( spl92_496
<=> n6 = sum(n0,n6) ),
introduced(definition,[new_symbols(definition,[spl92_496])],[avatar_definition]) ).
fof(f2950,plain,
spl92_496,
inference(avatar_split_clause,[],[f465,f2947]) ).
fof(f2952,definition,
( spl92_497
<=> n5 = sum(n0,n5) ),
introduced(definition,[new_symbols(definition,[spl92_497])],[avatar_definition]) ).
fof(f2955,plain,
spl92_497,
inference(avatar_split_clause,[],[f466,f2952]) ).
fof(f2957,definition,
( spl92_498
<=> n4 = sum(n0,n4) ),
introduced(definition,[new_symbols(definition,[spl92_498])],[avatar_definition]) ).
fof(f2960,plain,
spl92_498,
inference(avatar_split_clause,[],[f467,f2957]) ).
fof(f2962,definition,
( spl92_499
<=> n3 = sum(n0,n3) ),
introduced(definition,[new_symbols(definition,[spl92_499])],[avatar_definition]) ).
fof(f2965,plain,
spl92_499,
inference(avatar_split_clause,[],[f468,f2962]) ).
fof(f2967,definition,
( spl92_500
<=> n2 = sum(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl92_500])],[avatar_definition]) ).
fof(f2970,plain,
spl92_500,
inference(avatar_split_clause,[],[f469,f2967]) ).
fof(f2972,definition,
( spl92_501
<=> n1 = sum(n0,n1) ),
introduced(definition,[new_symbols(definition,[spl92_501])],[avatar_definition]) ).
fof(f2975,plain,
spl92_501,
inference(avatar_split_clause,[],[f470,f2972]) ).
fof(f2977,definition,
( spl92_502
<=> n0 = sum(n0,n0) ),
introduced(definition,[new_symbols(definition,[spl92_502])],[avatar_definition]) ).
fof(f2980,plain,
spl92_502,
inference(avatar_split_clause,[],[f471,f2977]) ).
fof(f2982,definition,
( spl92_503
<=> n14 = pred(n15) ),
introduced(definition,[new_symbols(definition,[spl92_503])],[avatar_definition]) ).
fof(f2985,plain,
spl92_503,
inference(avatar_split_clause,[],[f472,f2982]) ).
fof(f2987,definition,
( spl92_504
<=> n13 = pred(n14) ),
introduced(definition,[new_symbols(definition,[spl92_504])],[avatar_definition]) ).
fof(f2990,plain,
spl92_504,
inference(avatar_split_clause,[],[f473,f2987]) ).
fof(f2992,definition,
( spl92_505
<=> n12 = pred(n13) ),
introduced(definition,[new_symbols(definition,[spl92_505])],[avatar_definition]) ).
fof(f2995,plain,
spl92_505,
inference(avatar_split_clause,[],[f474,f2992]) ).
fof(f2997,definition,
( spl92_506
<=> n11 = pred(n12) ),
introduced(definition,[new_symbols(definition,[spl92_506])],[avatar_definition]) ).
fof(f3000,plain,
spl92_506,
inference(avatar_split_clause,[],[f475,f2997]) ).
fof(f3002,definition,
( spl92_507
<=> n10 = pred(n11) ),
introduced(definition,[new_symbols(definition,[spl92_507])],[avatar_definition]) ).
fof(f3005,plain,
spl92_507,
inference(avatar_split_clause,[],[f476,f3002]) ).
fof(f3007,definition,
( spl92_508
<=> n9 = pred(n10) ),
introduced(definition,[new_symbols(definition,[spl92_508])],[avatar_definition]) ).
fof(f3010,plain,
spl92_508,
inference(avatar_split_clause,[],[f477,f3007]) ).
fof(f3012,definition,
( spl92_509
<=> n8 = pred(n9) ),
introduced(definition,[new_symbols(definition,[spl92_509])],[avatar_definition]) ).
fof(f3015,plain,
spl92_509,
inference(avatar_split_clause,[],[f478,f3012]) ).
fof(f3017,definition,
( spl92_510
<=> n7 = pred(n8) ),
introduced(definition,[new_symbols(definition,[spl92_510])],[avatar_definition]) ).
fof(f3020,plain,
spl92_510,
inference(avatar_split_clause,[],[f479,f3017]) ).
fof(f3022,definition,
( spl92_511
<=> n6 = pred(n7) ),
introduced(definition,[new_symbols(definition,[spl92_511])],[avatar_definition]) ).
fof(f3025,plain,
spl92_511,
inference(avatar_split_clause,[],[f480,f3022]) ).
fof(f3027,definition,
( spl92_512
<=> n5 = pred(n6) ),
introduced(definition,[new_symbols(definition,[spl92_512])],[avatar_definition]) ).
fof(f3030,plain,
spl92_512,
inference(avatar_split_clause,[],[f481,f3027]) ).
fof(f3032,definition,
( spl92_513
<=> n4 = pred(n5) ),
introduced(definition,[new_symbols(definition,[spl92_513])],[avatar_definition]) ).
fof(f3035,plain,
spl92_513,
inference(avatar_split_clause,[],[f482,f3032]) ).
fof(f3037,definition,
( spl92_514
<=> n3 = pred(n4) ),
introduced(definition,[new_symbols(definition,[spl92_514])],[avatar_definition]) ).
fof(f3040,plain,
spl92_514,
inference(avatar_split_clause,[],[f483,f3037]) ).
fof(f3042,definition,
( spl92_515
<=> n2 = pred(n3) ),
introduced(definition,[new_symbols(definition,[spl92_515])],[avatar_definition]) ).
fof(f3045,plain,
spl92_515,
inference(avatar_split_clause,[],[f484,f3042]) ).
fof(f3047,definition,
( spl92_516
<=> n1 = pred(n2) ),
introduced(definition,[new_symbols(definition,[spl92_516])],[avatar_definition]) ).
fof(f3050,plain,
spl92_516,
inference(avatar_split_clause,[],[f485,f3047]) ).
fof(f3052,definition,
( spl92_517
<=> n0 = pred(n1) ),
introduced(definition,[new_symbols(definition,[spl92_517])],[avatar_definition]) ).
fof(f3055,plain,
spl92_517,
inference(avatar_split_clause,[],[f486,f3052]) ).
fof(f3057,definition,
( spl92_518
<=> n15 = pred(n0) ),
introduced(definition,[new_symbols(definition,[spl92_518])],[avatar_definition]) ).
fof(f3060,plain,
spl92_518,
inference(avatar_split_clause,[],[f487,f3057]) ).
fof(f3062,definition,
( spl92_519
<=> n0 = succ(n15) ),
introduced(definition,[new_symbols(definition,[spl92_519])],[avatar_definition]) ).
fof(f3065,plain,
spl92_519,
inference(avatar_split_clause,[],[f488,f3062]) ).
fof(f3067,definition,
( spl92_520
<=> succ(n14) = n15 ),
introduced(definition,[new_symbols(definition,[spl92_520])],[avatar_definition]) ).
fof(f3070,plain,
spl92_520,
inference(avatar_split_clause,[],[f489,f3067]) ).
fof(f3072,definition,
( spl92_521
<=> succ(n13) = n14 ),
introduced(definition,[new_symbols(definition,[spl92_521])],[avatar_definition]) ).
fof(f3075,plain,
spl92_521,
inference(avatar_split_clause,[],[f490,f3072]) ).
fof(f3077,definition,
( spl92_522
<=> succ(n12) = n13 ),
introduced(definition,[new_symbols(definition,[spl92_522])],[avatar_definition]) ).
fof(f3080,plain,
spl92_522,
inference(avatar_split_clause,[],[f491,f3077]) ).
fof(f3082,definition,
( spl92_523
<=> succ(n11) = n12 ),
introduced(definition,[new_symbols(definition,[spl92_523])],[avatar_definition]) ).
fof(f3085,plain,
spl92_523,
inference(avatar_split_clause,[],[f492,f3082]) ).
fof(f3087,definition,
( spl92_524
<=> succ(n10) = n11 ),
introduced(definition,[new_symbols(definition,[spl92_524])],[avatar_definition]) ).
fof(f3090,plain,
spl92_524,
inference(avatar_split_clause,[],[f493,f3087]) ).
fof(f3092,definition,
( spl92_525
<=> succ(n9) = n10 ),
introduced(definition,[new_symbols(definition,[spl92_525])],[avatar_definition]) ).
fof(f3095,plain,
spl92_525,
inference(avatar_split_clause,[],[f494,f3092]) ).
fof(f3097,definition,
( spl92_526
<=> succ(n8) = n9 ),
introduced(definition,[new_symbols(definition,[spl92_526])],[avatar_definition]) ).
fof(f3100,plain,
spl92_526,
inference(avatar_split_clause,[],[f495,f3097]) ).
fof(f3102,definition,
( spl92_527
<=> succ(n7) = n8 ),
introduced(definition,[new_symbols(definition,[spl92_527])],[avatar_definition]) ).
fof(f3105,plain,
spl92_527,
inference(avatar_split_clause,[],[f496,f3102]) ).
fof(f3107,definition,
( spl92_528
<=> succ(n6) = n7 ),
introduced(definition,[new_symbols(definition,[spl92_528])],[avatar_definition]) ).
fof(f3110,plain,
spl92_528,
inference(avatar_split_clause,[],[f497,f3107]) ).
fof(f3112,definition,
( spl92_529
<=> succ(n5) = n6 ),
introduced(definition,[new_symbols(definition,[spl92_529])],[avatar_definition]) ).
fof(f3115,plain,
spl92_529,
inference(avatar_split_clause,[],[f498,f3112]) ).
fof(f3117,definition,
( spl92_530
<=> succ(n4) = n5 ),
introduced(definition,[new_symbols(definition,[spl92_530])],[avatar_definition]) ).
fof(f3120,plain,
spl92_530,
inference(avatar_split_clause,[],[f499,f3117]) ).
fof(f3122,definition,
( spl92_531
<=> succ(n3) = n4 ),
introduced(definition,[new_symbols(definition,[spl92_531])],[avatar_definition]) ).
fof(f3125,plain,
spl92_531,
inference(avatar_split_clause,[],[f500,f3122]) ).
fof(f3127,definition,
( spl92_532
<=> succ(n2) = n3 ),
introduced(definition,[new_symbols(definition,[spl92_532])],[avatar_definition]) ).
fof(f3130,plain,
spl92_532,
inference(avatar_split_clause,[],[f501,f3127]) ).
fof(f3132,definition,
( spl92_533
<=> succ(n1) = n2 ),
introduced(definition,[new_symbols(definition,[spl92_533])],[avatar_definition]) ).
fof(f3135,plain,
spl92_533,
inference(avatar_split_clause,[],[f502,f3132]) ).
fof(f3137,definition,
( spl92_534
<=>