%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM375+1.025 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:19:17 PM UTC 2026
% Result : Timeout 295.08s 37.80s
% Output : None
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f0,axiom,
? [X,Y,Z] :
( n24 != n25
& n23 != n25
& n23 != n24
& n22 != n25
& n22 != n24
& n22 != n23
& n21 != n25
& n21 != n24
& n21 != n23
& n21 != n22
& n20 != n25
& n20 != n24
& n20 != n23
& n20 != n22
& n20 != n21
& n19 != n25
& n19 != n24
& n19 != n23
& n19 != n22
& n19 != n21
& n19 != n20
& n18 != n25
& n18 != n24
& n18 != n23
& n18 != n22
& n18 != n21
& n18 != n20
& n18 != n19
& n17 != n25
& n17 != n24
& n17 != n23
& n17 != n22
& n17 != n21
& n17 != n20
& n17 != n19
& n17 != n18
& n16 != n25
& n16 != n24
& n16 != n23
& n16 != n22
& n16 != n21
& n16 != n20
& n16 != n19
& n16 != n18
& n16 != n17
& n15 != n25
& n15 != n24
& n15 != n23
& n15 != n22
& n15 != n21
& n15 != n20
& n15 != n19
& n15 != n18
& n15 != n17
& n15 != n16
& n14 != n25
& n14 != n24
& n14 != n23
& n14 != n22
& n14 != n21
& n14 != n20
& n14 != n19
& n14 != n18
& n14 != n17
& n14 != n16
& n14 != n15
& n13 != n25
& n13 != n24
& n13 != n23
& n13 != n22
& n13 != n21
& n13 != n20
& n13 != n19
& n13 != n18
& n13 != n17
& n13 != n16
& n13 != n15
& n13 != n14
& n12 != n25
& n12 != n24
& n12 != n23
& n12 != n22
& n12 != n21
& n12 != n20
& n12 != n19
& n12 != n18
& n12 != n17
& n12 != n16
& n12 != n15
& n12 != n14
& n12 != n13
& n11 != n25
& n11 != n24
& n11 != n23
& n11 != n22
& n11 != n21
& n11 != n20
& n11 != n19
& n11 != n18
& n11 != n17
& n11 != n16
& n11 != n15
& n11 != n14
& n11 != n13
& n11 != n12
& n10 != n25
& n10 != n24
& n10 != n23
& n10 != n22
& n10 != n21
& n10 != n20
& n10 != n19
& n10 != n18
& n10 != n17
& n10 != n16
& n10 != n15
& n10 != n14
& n10 != n13
& n10 != n12
& n10 != n11
& n9 != n25
& n9 != n24
& n9 != n23
& n9 != n22
& n9 != n21
& n9 != n20
& n9 != n19
& n9 != n18
& n9 != n17
& n9 != n16
& n9 != n15
& n9 != n14
& n9 != n13
& n9 != n12
& n9 != n11
& n9 != n10
& n8 != n25
& n8 != n24
& n8 != n23
& n8 != n22
& n8 != n21
& n8 != n20
& n8 != n19
& n8 != n18
& n8 != n17
& n8 != n16
& n8 != n15
& n8 != n14
& n8 != n13
& n8 != n12
& n8 != n11
& n8 != n10
& n8 != n9
& n7 != n25
& n7 != n24
& n7 != n23
& n7 != n22
& n7 != n21
& n7 != n20
& n7 != n19
& n7 != n18
& n7 != n17
& n7 != n16
& n7 != n15
& n7 != n14
& n7 != n13
& n7 != n12
& n7 != n11
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n25
& n6 != n24
& n6 != n23
& n6 != n22
& n6 != n21
& n6 != n20
& n6 != n19
& n6 != n18
& n6 != n17
& n6 != n16
& n6 != n15
& n6 != n14
& n6 != n13
& n6 != n12
& n6 != n11
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n25
& n5 != n24
& n5 != n23
& n5 != n22
& n5 != n21
& n5 != n20
& n5 != n19
& n5 != n18
& n5 != n17
& n5 != n16
& n5 != n15
& n5 != n14
& n5 != n13
& n5 != n12
& n5 != n11
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n25
& n4 != n24
& n4 != n23
& n4 != n22
& n4 != n21
& n4 != n20
& n4 != n19
& n4 != n18
& n4 != n17
& n4 != n16
& n4 != n15
& n4 != n14
& n4 != n13
& n4 != n12
& n4 != n11
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n25
& n3 != n24
& n3 != n23
& n3 != n22
& n3 != n21
& n3 != n20
& n3 != n19
& n3 != n18
& n3 != n17
& n3 != n16
& n3 != n15
& n3 != n14
& n3 != n13
& n3 != n12
& n3 != n11
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n25
& n2 != n24
& n2 != n23
& n2 != n22
& n2 != n21
& n2 != n20
& n2 != n19
& n2 != n18
& n2 != n17
& n2 != n16
& n2 != n15
& n2 != n14
& n2 != n13
& n2 != n12
& n2 != n11
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n25
& n1 != n24
& n1 != n23
& n1 != n22
& n1 != n21
& n1 != n20
& n1 != n19
& n1 != n18
& n1 != n17
& n1 != n16
& n1 != n15
& n1 != n14
& n1 != n13
& n1 != n12
& n1 != n11
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n25
& n0 != n24
& n0 != n23
& n0 != n22
& n0 != n21
& n0 != n20
& n0 != n19
& n0 != n18
& n0 != n17
& n0 != n16
& n0 != n15
& n0 != n14
& n0 != n13
& n0 != n12
& n0 != n11
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& Z != n25
& Z != n24
& Z != n23
& Z != n22
& Z != n21
& Z != n20
& Z != n19
& Z != n18
& Z != n17
& Z != n16
& Z != n15
& Z != n14
& Z != n13
& Z != n12
& Z != n11
& Z != n10
& Z != n9
& Z != n8
& Z != n7
& Z != n6
& Z != n5
& Z != n4
& Z != n3
& Z != n2
& Z != n1
& Z != n0
& Z = sum(pred(sum(X,succ(Y))),sum(Y,pred(sum(X,Y))))
& ( Y = n25
| Y = n24
| Y = n23
| Y = n22
| Y = n21
| Y = n20
| Y = n19
| Y = n18
| Y = n17
| Y = n16
| Y = n15
| Y = n14
| Y = n13
| Y = n12
| Y = n11
| Y = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n25
| X = n24
| X = n23
| X = n22
| X = n21
| X = n20
| X = n19
| X = n18
| X = n17
| X = n16
| X = n15
| X = n14
| X = n13
| X = n12
| X = n11
| X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n25,n25) = n24
& sum(n25,n24) = n23
& sum(n25,n23) = n22
& sum(n25,n22) = n21
& sum(n25,n21) = n20
& sum(n25,n20) = n19
& sum(n25,n19) = n18
& sum(n25,n18) = n17
& sum(n25,n17) = n16
& sum(n25,n16) = n15
& sum(n25,n15) = n14
& sum(n25,n14) = n13
& sum(n25,n13) = n12
& sum(n25,n12) = n11
& sum(n25,n11) = n10
& sum(n25,n10) = n9
& sum(n25,n9) = n8
& sum(n25,n8) = n7
& sum(n25,n7) = n6
& sum(n25,n6) = n5
& sum(n25,n5) = n4
& sum(n25,n4) = n3
& sum(n25,n3) = n2
& sum(n25,n2) = n1
& sum(n25,n1) = n0
& sum(n25,n0) = n25
& sum(n24,n25) = n23
& sum(n24,n24) = n22
& sum(n24,n23) = n21
& sum(n24,n22) = n20
& sum(n24,n21) = n19
& sum(n24,n20) = n18
& sum(n24,n19) = n17
& sum(n24,n18) = n16
& sum(n24,n17) = n15
& sum(n24,n16) = n14
& sum(n24,n15) = n13
& sum(n24,n14) = n12
& sum(n24,n13) = n11
& sum(n24,n12) = n10
& sum(n24,n11) = n9
& sum(n24,n10) = n8
& sum(n24,n9) = n7
& sum(n24,n8) = n6
& sum(n24,n7) = n5
& sum(n24,n6) = n4
& sum(n24,n5) = n3
& sum(n24,n4) = n2
& sum(n24,n3) = n1
& sum(n24,n2) = n0
& sum(n24,n1) = n25
& sum(n24,n0) = n24
& sum(n23,n25) = n22
& sum(n23,n24) = n21
& sum(n23,n23) = n20
& sum(n23,n22) = n19
& sum(n23,n21) = n18
& sum(n23,n20) = n17
& sum(n23,n19) = n16
& sum(n23,n18) = n15
& sum(n23,n17) = n14
& sum(n23,n16) = n13
& sum(n23,n15) = n12
& sum(n23,n14) = n11
& sum(n23,n13) = n10
& sum(n23,n12) = n9
& sum(n23,n11) = n8
& sum(n23,n10) = n7
& sum(n23,n9) = n6
& sum(n23,n8) = n5
& sum(n23,n7) = n4
& sum(n23,n6) = n3
& sum(n23,n5) = n2
& sum(n23,n4) = n1
& sum(n23,n3) = n0
& sum(n23,n2) = n25
& sum(n23,n1) = n24
& sum(n23,n0) = n23
& sum(n22,n25) = n21
& sum(n22,n24) = n20
& sum(n22,n23) = n19
& sum(n22,n22) = n18
& sum(n22,n21) = n17
& sum(n22,n20) = n16
& sum(n22,n19) = n15
& sum(n22,n18) = n14
& sum(n22,n17) = n13
& sum(n22,n16) = n12
& sum(n22,n15) = n11
& sum(n22,n14) = n10
& sum(n22,n13) = n9
& sum(n22,n12) = n8
& sum(n22,n11) = n7
& sum(n22,n10) = n6
& sum(n22,n9) = n5
& sum(n22,n8) = n4
& sum(n22,n7) = n3
& sum(n22,n6) = n2
& sum(n22,n5) = n1
& sum(n22,n4) = n0
& sum(n22,n3) = n25
& sum(n22,n2) = n24
& sum(n22,n1) = n23
& sum(n22,n0) = n22
& sum(n21,n25) = n20
& sum(n21,n24) = n19
& sum(n21,n23) = n18
& sum(n21,n22) = n17
& sum(n21,n21) = n16
& sum(n21,n20) = n15
& sum(n21,n19) = n14
& sum(n21,n18) = n13
& sum(n21,n17) = n12
& sum(n21,n16) = n11
& sum(n21,n15) = n10
& sum(n21,n14) = n9
& sum(n21,n13) = n8
& sum(n21,n12) = n7
& sum(n21,n11) = n6
& sum(n21,n10) = n5
& sum(n21,n9) = n4
& sum(n21,n8) = n3
& sum(n21,n7) = n2
& sum(n21,n6) = n1
& sum(n21,n5) = n0
& sum(n21,n4) = n25
& sum(n21,n3) = n24
& sum(n21,n2) = n23
& sum(n21,n1) = n22
& sum(n21,n0) = n21
& sum(n20,n25) = n19
& sum(n20,n24) = n18
& sum(n20,n23) = n17
& sum(n20,n22) = n16
& sum(n20,n21) = n15
& sum(n20,n20) = n14
& sum(n20,n19) = n13
& sum(n20,n18) = n12
& sum(n20,n17) = n11
& sum(n20,n16) = n10
& sum(n20,n15) = n9
& sum(n20,n14) = n8
& sum(n20,n13) = n7
& sum(n20,n12) = n6
& sum(n20,n11) = n5
& sum(n20,n10) = n4
& sum(n20,n9) = n3
& sum(n20,n8) = n2
& sum(n20,n7) = n1
& sum(n20,n6) = n0
& sum(n20,n5) = n25
& sum(n20,n4) = n24
& sum(n20,n3) = n23
& sum(n20,n2) = n22
& sum(n20,n1) = n21
& sum(n20,n0) = n20
& sum(n19,n25) = n18
& sum(n19,n24) = n17
& sum(n19,n23) = n16
& sum(n19,n22) = n15
& sum(n19,n21) = n14
& sum(n19,n20) = n13
& sum(n19,n19) = n12
& sum(n19,n18) = n11
& sum(n19,n17) = n10
& sum(n19,n16) = n9
& sum(n19,n15) = n8
& sum(n19,n14) = n7
& sum(n19,n13) = n6
& sum(n19,n12) = n5
& sum(n19,n11) = n4
& sum(n19,n10) = n3
& sum(n19,n9) = n2
& sum(n19,n8) = n1
& sum(n19,n7) = n0
& sum(n19,n6) = n25
& sum(n19,n5) = n24
& sum(n19,n4) = n23
& sum(n19,n3) = n22
& sum(n19,n2) = n21
& sum(n19,n1) = n20
& sum(n19,n0) = n19
& sum(n18,n25) = n17
& sum(n18,n24) = n16
& sum(n18,n23) = n15
& sum(n18,n22) = n14
& sum(n18,n21) = n13
& sum(n18,n20) = n12
& sum(n18,n19) = n11
& sum(n18,n18) = n10
& sum(n18,n17) = n9
& sum(n18,n16) = n8
& sum(n18,n15) = n7
& sum(n18,n14) = n6
& sum(n18,n13) = n5
& sum(n18,n12) = n4
& sum(n18,n11) = n3
& sum(n18,n10) = n2
& sum(n18,n9) = n1
& sum(n18,n8) = n0
& sum(n18,n7) = n25
& sum(n18,n6) = n24
& sum(n18,n5) = n23
& sum(n18,n4) = n22
& sum(n18,n3) = n21
& sum(n18,n2) = n20
& sum(n18,n1) = n19
& sum(n18,n0) = n18
& sum(n17,n25) = n16
& sum(n17,n24) = n15
& sum(n17,n23) = n14
& sum(n17,n22) = n13
& sum(n17,n21) = n12
& sum(n17,n20) = n11
& sum(n17,n19) = n10
& sum(n17,n18) = n9
& sum(n17,n17) = n8
& sum(n17,n16) = n7
& sum(n17,n15) = n6
& sum(n17,n14) = n5
& sum(n17,n13) = n4
& sum(n17,n12) = n3
& sum(n17,n11) = n2
& sum(n17,n10) = n1
& sum(n17,n9) = n0
& sum(n17,n8) = n25
& sum(n17,n7) = n24
& sum(n17,n6) = n23
& sum(n17,n5) = n22
& sum(n17,n4) = n21
& sum(n17,n3) = n20
& sum(n17,n2) = n19
& sum(n17,n1) = n18
& sum(n17,n0) = n17
& sum(n16,n25) = n15
& sum(n16,n24) = n14
& sum(n16,n23) = n13
& sum(n16,n22) = n12
& sum(n16,n21) = n11
& sum(n16,n20) = n10
& sum(n16,n19) = n9
& sum(n16,n18) = n8
& sum(n16,n17) = n7
& sum(n16,n16) = n6
& sum(n16,n15) = n5
& sum(n16,n14) = n4
& sum(n16,n13) = n3
& sum(n16,n12) = n2
& sum(n16,n11) = n1
& sum(n16,n10) = n0
& sum(n16,n9) = n25
& sum(n16,n8) = n24
& sum(n16,n7) = n23
& sum(n16,n6) = n22
& sum(n16,n5) = n21
& sum(n16,n4) = n20
& sum(n16,n3) = n19
& sum(n16,n2) = n18
& sum(n16,n1) = n17
& sum(n16,n0) = n16
& sum(n15,n25) = n14
& sum(n15,n24) = n13
& sum(n15,n23) = n12
& sum(n15,n22) = n11
& sum(n15,n21) = n10
& sum(n15,n20) = n9
& sum(n15,n19) = n8
& sum(n15,n18) = n7
& sum(n15,n17) = n6
& sum(n15,n16) = n5
& sum(n15,n15) = n4
& sum(n15,n14) = n3
& sum(n15,n13) = n2
& sum(n15,n12) = n1
& sum(n15,n11) = n0
& sum(n15,n10) = n25
& sum(n15,n9) = n24
& sum(n15,n8) = n23
& sum(n15,n7) = n22
& sum(n15,n6) = n21
& sum(n15,n5) = n20
& sum(n15,n4) = n19
& sum(n15,n3) = n18
& sum(n15,n2) = n17
& sum(n15,n1) = n16
& sum(n15,n0) = n15
& sum(n14,n25) = n13
& sum(n14,n24) = n12
& sum(n14,n23) = n11
& sum(n14,n22) = n10
& sum(n14,n21) = n9
& sum(n14,n20) = n8
& sum(n14,n19) = n7
& sum(n14,n18) = n6
& sum(n14,n17) = n5
& sum(n14,n16) = n4
& sum(n14,n15) = n3
& sum(n14,n14) = n2
& sum(n14,n13) = n1
& sum(n14,n12) = n0
& sum(n14,n11) = n25
& sum(n14,n10) = n24
& sum(n14,n9) = n23
& sum(n14,n8) = n22
& sum(n14,n7) = n21
& sum(n14,n6) = n20
& sum(n14,n5) = n19
& sum(n14,n4) = n18
& sum(n14,n3) = n17
& sum(n14,n2) = n16
& sum(n14,n1) = n15
& sum(n14,n0) = n14
& sum(n13,n25) = n12
& sum(n13,n24) = n11
& sum(n13,n23) = n10
& sum(n13,n22) = n9
& sum(n13,n21) = n8
& sum(n13,n20) = n7
& sum(n13,n19) = n6
& sum(n13,n18) = n5
& sum(n13,n17) = n4
& sum(n13,n16) = n3
& sum(n13,n15) = n2
& sum(n13,n14) = n1
& sum(n13,n13) = n0
& sum(n13,n12) = n25
& sum(n13,n11) = n24
& sum(n13,n10) = n23
& sum(n13,n9) = n22
& sum(n13,n8) = n21
& sum(n13,n7) = n20
& sum(n13,n6) = n19
& sum(n13,n5) = n18
& sum(n13,n4) = n17
& sum(n13,n3) = n16
& sum(n13,n2) = n15
& sum(n13,n1) = n14
& sum(n13,n0) = n13
& sum(n12,n25) = n11
& sum(n12,n24) = n10
& sum(n12,n23) = n9
& sum(n12,n22) = n8
& sum(n12,n21) = n7
& sum(n12,n20) = n6
& sum(n12,n19) = n5
& sum(n12,n18) = n4
& sum(n12,n17) = n3
& sum(n12,n16) = n2
& sum(n12,n15) = n1
& sum(n12,n14) = n0
& sum(n12,n13) = n25
& sum(n12,n12) = n24
& sum(n12,n11) = n23
& sum(n12,n10) = n22
& sum(n12,n9) = n21
& sum(n12,n8) = n20
& sum(n12,n7) = n19
& sum(n12,n6) = n18
& sum(n12,n5) = n17
& sum(n12,n4) = n16
& sum(n12,n3) = n15
& sum(n12,n2) = n14
& sum(n12,n1) = n13
& sum(n12,n0) = n12
& sum(n11,n25) = n10
& sum(n11,n24) = n9
& sum(n11,n23) = n8
& sum(n11,n22) = n7
& sum(n11,n21) = n6
& sum(n11,n20) = n5
& sum(n11,n19) = n4
& sum(n11,n18) = n3
& sum(n11,n17) = n2
& sum(n11,n16) = n1
& sum(n11,n15) = n0
& sum(n11,n14) = n25
& sum(n11,n13) = n24
& sum(n11,n12) = n23
& sum(n11,n11) = n22
& sum(n11,n10) = n21
& sum(n11,n9) = n20
& sum(n11,n8) = n19
& sum(n11,n7) = n18
& sum(n11,n6) = n17
& sum(n11,n5) = n16
& sum(n11,n4) = n15
& sum(n11,n3) = n14
& sum(n11,n2) = n13
& sum(n11,n1) = n12
& sum(n11,n0) = n11
& sum(n10,n25) = n9
& sum(n10,n24) = n8
& sum(n10,n23) = n7
& sum(n10,n22) = n6
& sum(n10,n21) = n5
& sum(n10,n20) = n4
& sum(n10,n19) = n3
& sum(n10,n18) = n2
& sum(n10,n17) = n1
& sum(n10,n16) = n0
& sum(n10,n15) = n25
& sum(n10,n14) = n24
& sum(n10,n13) = n23
& sum(n10,n12) = n22
& sum(n10,n11) = n21
& sum(n10,n10) = n20
& sum(n10,n9) = n19
& sum(n10,n8) = n18
& sum(n10,n7) = n17
& sum(n10,n6) = n16
& sum(n10,n5) = n15
& sum(n10,n4) = n14
& sum(n10,n3) = n13
& sum(n10,n2) = n12
& sum(n10,n1) = n11
& sum(n10,n0) = n10
& sum(n9,n25) = n8
& sum(n9,n24) = n7
& sum(n9,n23) = n6
& sum(n9,n22) = n5
& sum(n9,n21) = n4
& sum(n9,n20) = n3
& sum(n9,n19) = n2
& sum(n9,n18) = n1
& sum(n9,n17) = n0
& sum(n9,n16) = n25
& sum(n9,n15) = n24
& sum(n9,n14) = n23
& sum(n9,n13) = n22
& sum(n9,n12) = n21
& sum(n9,n11) = n20
& sum(n9,n10) = n19
& sum(n9,n9) = n18
& sum(n9,n8) = n17
& sum(n9,n7) = n16
& sum(n9,n6) = n15
& sum(n9,n5) = n14
& sum(n9,n4) = n13
& sum(n9,n3) = n12
& sum(n9,n2) = n11
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n25) = n7
& sum(n8,n24) = n6
& sum(n8,n23) = n5
& sum(n8,n22) = n4
& sum(n8,n21) = n3
& sum(n8,n20) = n2
& sum(n8,n19) = n1
& sum(n8,n18) = n0
& sum(n8,n17) = n25
& sum(n8,n16) = n24
& sum(n8,n15) = n23
& sum(n8,n14) = n22
& sum(n8,n13) = n21
& sum(n8,n12) = n20
& sum(n8,n11) = n19
& sum(n8,n10) = n18
& sum(n8,n9) = n17
& sum(n8,n8) = n16
& sum(n8,n7) = n15
& sum(n8,n6) = n14
& sum(n8,n5) = n13
& sum(n8,n4) = n12
& sum(n8,n3) = n11
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n25) = n6
& sum(n7,n24) = n5
& sum(n7,n23) = n4
& sum(n7,n22) = n3
& sum(n7,n21) = n2
& sum(n7,n20) = n1
& sum(n7,n19) = n0
& sum(n7,n18) = n25
& sum(n7,n17) = n24
& sum(n7,n16) = n23
& sum(n7,n15) = n22
& sum(n7,n14) = n21
& sum(n7,n13) = n20
& sum(n7,n12) = n19
& sum(n7,n11) = n18
& sum(n7,n10) = n17
& sum(n7,n9) = n16
& sum(n7,n8) = n15
& sum(n7,n7) = n14
& sum(n7,n6) = n13
& sum(n7,n5) = n12
& sum(n7,n4) = n11
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n25) = n5
& sum(n6,n24) = n4
& sum(n6,n23) = n3
& sum(n6,n22) = n2
& sum(n6,n21) = n1
& sum(n6,n20) = n0
& sum(n6,n19) = n25
& sum(n6,n18) = n24
& sum(n6,n17) = n23
& sum(n6,n16) = n22
& sum(n6,n15) = n21
& sum(n6,n14) = n20
& sum(n6,n13) = n19
& sum(n6,n12) = n18
& sum(n6,n11) = n17
& sum(n6,n10) = n16
& sum(n6,n9) = n15
& sum(n6,n8) = n14
& sum(n6,n7) = n13
& sum(n6,n6) = n12
& sum(n6,n5) = n11
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n25) = n4
& sum(n5,n24) = n3
& sum(n5,n23) = n2
& sum(n5,n22) = n1
& sum(n5,n21) = n0
& sum(n5,n20) = n25
& sum(n5,n19) = n24
& sum(n5,n18) = n23
& sum(n5,n17) = n22
& sum(n5,n16) = n21
& sum(n5,n15) = n20
& sum(n5,n14) = n19
& sum(n5,n13) = n18
& sum(n5,n12) = n17
& sum(n5,n11) = n16
& sum(n5,n10) = n15
& sum(n5,n9) = n14
& sum(n5,n8) = n13
& sum(n5,n7) = n12
& sum(n5,n6) = n11
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n25) = n3
& sum(n4,n24) = n2
& sum(n4,n23) = n1
& sum(n4,n22) = n0
& sum(n4,n21) = n25
& sum(n4,n20) = n24
& sum(n4,n19) = n23
& sum(n4,n18) = n22
& sum(n4,n17) = n21
& sum(n4,n16) = n20
& sum(n4,n15) = n19
& sum(n4,n14) = n18
& sum(n4,n13) = n17
& sum(n4,n12) = n16
& sum(n4,n11) = n15
& sum(n4,n10) = n14
& sum(n4,n9) = n13
& sum(n4,n8) = n12
& sum(n4,n7) = n11
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n25) = n2
& sum(n3,n24) = n1
& sum(n3,n23) = n0
& sum(n3,n22) = n25
& sum(n3,n21) = n24
& sum(n3,n20) = n23
& sum(n3,n19) = n22
& sum(n3,n18) = n21
& sum(n3,n17) = n20
& sum(n3,n16) = n19
& sum(n3,n15) = n18
& sum(n3,n14) = n17
& sum(n3,n13) = n16
& sum(n3,n12) = n15
& sum(n3,n11) = n14
& sum(n3,n10) = n13
& sum(n3,n9) = n12
& sum(n3,n8) = n11
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n25) = n1
& sum(n2,n24) = n0
& sum(n2,n23) = n25
& sum(n2,n22) = n24
& sum(n2,n21) = n23
& sum(n2,n20) = n22
& sum(n2,n19) = n21
& sum(n2,n18) = n20
& sum(n2,n17) = n19
& sum(n2,n16) = n18
& sum(n2,n15) = n17
& sum(n2,n14) = n16
& sum(n2,n13) = n15
& sum(n2,n12) = n14
& sum(n2,n11) = n13
& sum(n2,n10) = n12
& sum(n2,n9) = n11
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n25) = n0
& sum(n1,n24) = n25
& sum(n1,n23) = n24
& sum(n1,n22) = n23
& sum(n1,n21) = n22
& sum(n1,n20) = n21
& sum(n1,n19) = n20
& sum(n1,n18) = n19
& sum(n1,n17) = n18
& sum(n1,n16) = n17
& sum(n1,n15) = n16
& sum(n1,n14) = n15
& sum(n1,n13) = n14
& sum(n1,n12) = n13
& sum(n1,n11) = n12
& sum(n1,n10) = n11
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n25) = n25
& sum(n0,n24) = n24
& sum(n0,n23) = n23
& sum(n0,n22) = n22
& sum(n0,n21) = n21
& sum(n0,n20) = n20
& sum(n0,n19) = n19
& sum(n0,n18) = n18
& sum(n0,n17) = n17
& sum(n0,n16) = n16
& sum(n0,n15) = n15
& sum(n0,n14) = n14
& sum(n0,n13) = n13
& sum(n0,n12) = n12
& sum(n0,n11) = n11
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n25) = n24
& pred(n24) = n23
& pred(n23) = n22
& pred(n22) = n21
& pred(n21) = n20
& pred(n20) = n19
& pred(n19) = n18
& pred(n18) = n17
& pred(n17) = n16
& pred(n16) = n15
& pred(n15) = n14
& pred(n14) = n13
& pred(n13) = n12
& pred(n12) = n11
& pred(n11) = n10
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n25
& succ(n25) = n0
& succ(n24) = n25
& succ(n23) = n24
& succ(n22) = n23
& succ(n21) = n22
& succ(n20) = n21
& succ(n19) = n20
& succ(n18) = n19
& succ(n17) = n18
& succ(n16) = n17
& succ(n15) = n16
& succ(n14) = n15
& succ(n13) = n14
& succ(n12) = n13
& succ(n11) = n12
& succ(n10) = n11
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',try_satisfy_this) ).
fof(f0_nnf,plain,
? [X,Y,Z] :
( n24 != n25
& n23 != n25
& n23 != n24
& n22 != n25
& n22 != n24
& n22 != n23
& n21 != n25
& n21 != n24
& n21 != n23
& n21 != n22
& n20 != n25
& n20 != n24
& n20 != n23
& n20 != n22
& n20 != n21
& n19 != n25
& n19 != n24
& n19 != n23
& n19 != n22
& n19 != n21
& n19 != n20
& n18 != n25
& n18 != n24
& n18 != n23
& n18 != n22
& n18 != n21
& n18 != n20
& n18 != n19
& n17 != n25
& n17 != n24
& n17 != n23
& n17 != n22
& n17 != n21
& n17 != n20
& n17 != n19
& n17 != n18
& n16 != n25
& n16 != n24
& n16 != n23
& n16 != n22
& n16 != n21
& n16 != n20
& n16 != n19
& n16 != n18
& n16 != n17
& n15 != n25
& n15 != n24
& n15 != n23
& n15 != n22
& n15 != n21
& n15 != n20
& n15 != n19
& n15 != n18
& n15 != n17
& n15 != n16
& n14 != n25
& n14 != n24
& n14 != n23
& n14 != n22
& n14 != n21
& n14 != n20
& n14 != n19
& n14 != n18
& n14 != n17
& n14 != n16
& n14 != n15
& n13 != n25
& n13 != n24
& n13 != n23
& n13 != n22
& n13 != n21
& n13 != n20
& n13 != n19
& n13 != n18
& n13 != n17
& n13 != n16
& n13 != n15
& n13 != n14
& n12 != n25
& n12 != n24
& n12 != n23
& n12 != n22
& n12 != n21
& n12 != n20
& n12 != n19
& n12 != n18
& n12 != n17
& n12 != n16
& n12 != n15
& n12 != n14
& n12 != n13
& n11 != n25
& n11 != n24
& n11 != n23
& n11 != n22
& n11 != n21
& n11 != n20
& n11 != n19
& n11 != n18
& n11 != n17
& n11 != n16
& n11 != n15
& n11 != n14
& n11 != n13
& n11 != n12
& n10 != n25
& n10 != n24
& n10 != n23
& n10 != n22
& n10 != n21
& n10 != n20
& n10 != n19
& n10 != n18
& n10 != n17
& n10 != n16
& n10 != n15
& n10 != n14
& n10 != n13
& n10 != n12
& n10 != n11
& n9 != n25
& n9 != n24
& n9 != n23
& n9 != n22
& n9 != n21
& n9 != n20
& n9 != n19
& n9 != n18
& n9 != n17
& n9 != n16
& n9 != n15
& n9 != n14
& n9 != n13
& n9 != n12
& n9 != n11
& n9 != n10
& n8 != n25
& n8 != n24
& n8 != n23
& n8 != n22
& n8 != n21
& n8 != n20
& n8 != n19
& n8 != n18
& n8 != n17
& n8 != n16
& n8 != n15
& n8 != n14
& n8 != n13
& n8 != n12
& n8 != n11
& n8 != n10
& n8 != n9
& n7 != n25
& n7 != n24
& n7 != n23
& n7 != n22
& n7 != n21
& n7 != n20
& n7 != n19
& n7 != n18
& n7 != n17
& n7 != n16
& n7 != n15
& n7 != n14
& n7 != n13
& n7 != n12
& n7 != n11
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n25
& n6 != n24
& n6 != n23
& n6 != n22
& n6 != n21
& n6 != n20
& n6 != n19
& n6 != n18
& n6 != n17
& n6 != n16
& n6 != n15
& n6 != n14
& n6 != n13
& n6 != n12
& n6 != n11
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n25
& n5 != n24
& n5 != n23
& n5 != n22
& n5 != n21
& n5 != n20
& n5 != n19
& n5 != n18
& n5 != n17
& n5 != n16
& n5 != n15
& n5 != n14
& n5 != n13
& n5 != n12
& n5 != n11
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n25
& n4 != n24
& n4 != n23
& n4 != n22
& n4 != n21
& n4 != n20
& n4 != n19
& n4 != n18
& n4 != n17
& n4 != n16
& n4 != n15
& n4 != n14
& n4 != n13
& n4 != n12
& n4 != n11
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n25
& n3 != n24
& n3 != n23
& n3 != n22
& n3 != n21
& n3 != n20
& n3 != n19
& n3 != n18
& n3 != n17
& n3 != n16
& n3 != n15
& n3 != n14
& n3 != n13
& n3 != n12
& n3 != n11
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n25
& n2 != n24
& n2 != n23
& n2 != n22
& n2 != n21
& n2 != n20
& n2 != n19
& n2 != n18
& n2 != n17
& n2 != n16
& n2 != n15
& n2 != n14
& n2 != n13
& n2 != n12
& n2 != n11
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n25
& n1 != n24
& n1 != n23
& n1 != n22
& n1 != n21
& n1 != n20
& n1 != n19
& n1 != n18
& n1 != n17
& n1 != n16
& n1 != n15
& n1 != n14
& n1 != n13
& n1 != n12
& n1 != n11
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n25
& n0 != n24
& n0 != n23
& n0 != n22
& n0 != n21
& n0 != n20
& n0 != n19
& n0 != n18
& n0 != n17
& n0 != n16
& n0 != n15
& n0 != n14
& n0 != n13
& n0 != n12
& n0 != n11
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& Z != n25
& Z != n24
& Z != n23
& Z != n22
& Z != n21
& Z != n20
& Z != n19
& Z != n18
& Z != n17
& Z != n16
& Z != n15
& Z != n14
& Z != n13
& Z != n12
& Z != n11
& Z != n10
& Z != n9
& Z != n8
& Z != n7
& Z != n6
& Z != n5
& Z != n4
& Z != n3
& Z != n2
& Z != n1
& Z != n0
& Z = sum(pred(sum(X,succ(Y))),sum(Y,pred(sum(X,Y))))
& ( Y = n25
| Y = n24
| Y = n23
| Y = n22
| Y = n21
| Y = n20
| Y = n19
| Y = n18
| Y = n17
| Y = n16
| Y = n15
| Y = n14
| Y = n13
| Y = n12
| Y = n11
| Y = n10
| Y = n9
| Y = n8
| Y = n7
| Y = n6
| Y = n5
| Y = n4
| Y = n3
| Y = n2
| Y = n1
| Y = n0 )
& ( X = n25
| X = n24
| X = n23
| X = n22
| X = n21
| X = n20
| X = n19
| X = n18
| X = n17
| X = n16
| X = n15
| X = n14
| X = n13
| X = n12
| X = n11
| X = n10
| X = n9
| X = n8
| X = n7
| X = n6
| X = n5
| X = n4
| X = n3
| X = n2
| X = n1
| X = n0 )
& sum(n25,n25) = n24
& sum(n25,n24) = n23
& sum(n25,n23) = n22
& sum(n25,n22) = n21
& sum(n25,n21) = n20
& sum(n25,n20) = n19
& sum(n25,n19) = n18
& sum(n25,n18) = n17
& sum(n25,n17) = n16
& sum(n25,n16) = n15
& sum(n25,n15) = n14
& sum(n25,n14) = n13
& sum(n25,n13) = n12
& sum(n25,n12) = n11
& sum(n25,n11) = n10
& sum(n25,n10) = n9
& sum(n25,n9) = n8
& sum(n25,n8) = n7
& sum(n25,n7) = n6
& sum(n25,n6) = n5
& sum(n25,n5) = n4
& sum(n25,n4) = n3
& sum(n25,n3) = n2
& sum(n25,n2) = n1
& sum(n25,n1) = n0
& sum(n25,n0) = n25
& sum(n24,n25) = n23
& sum(n24,n24) = n22
& sum(n24,n23) = n21
& sum(n24,n22) = n20
& sum(n24,n21) = n19
& sum(n24,n20) = n18
& sum(n24,n19) = n17
& sum(n24,n18) = n16
& sum(n24,n17) = n15
& sum(n24,n16) = n14
& sum(n24,n15) = n13
& sum(n24,n14) = n12
& sum(n24,n13) = n11
& sum(n24,n12) = n10
& sum(n24,n11) = n9
& sum(n24,n10) = n8
& sum(n24,n9) = n7
& sum(n24,n8) = n6
& sum(n24,n7) = n5
& sum(n24,n6) = n4
& sum(n24,n5) = n3
& sum(n24,n4) = n2
& sum(n24,n3) = n1
& sum(n24,n2) = n0
& sum(n24,n1) = n25
& sum(n24,n0) = n24
& sum(n23,n25) = n22
& sum(n23,n24) = n21
& sum(n23,n23) = n20
& sum(n23,n22) = n19
& sum(n23,n21) = n18
& sum(n23,n20) = n17
& sum(n23,n19) = n16
& sum(n23,n18) = n15
& sum(n23,n17) = n14
& sum(n23,n16) = n13
& sum(n23,n15) = n12
& sum(n23,n14) = n11
& sum(n23,n13) = n10
& sum(n23,n12) = n9
& sum(n23,n11) = n8
& sum(n23,n10) = n7
& sum(n23,n9) = n6
& sum(n23,n8) = n5
& sum(n23,n7) = n4
& sum(n23,n6) = n3
& sum(n23,n5) = n2
& sum(n23,n4) = n1
& sum(n23,n3) = n0
& sum(n23,n2) = n25
& sum(n23,n1) = n24
& sum(n23,n0) = n23
& sum(n22,n25) = n21
& sum(n22,n24) = n20
& sum(n22,n23) = n19
& sum(n22,n22) = n18
& sum(n22,n21) = n17
& sum(n22,n20) = n16
& sum(n22,n19) = n15
& sum(n22,n18) = n14
& sum(n22,n17) = n13
& sum(n22,n16) = n12
& sum(n22,n15) = n11
& sum(n22,n14) = n10
& sum(n22,n13) = n9
& sum(n22,n12) = n8
& sum(n22,n11) = n7
& sum(n22,n10) = n6
& sum(n22,n9) = n5
& sum(n22,n8) = n4
& sum(n22,n7) = n3
& sum(n22,n6) = n2
& sum(n22,n5) = n1
& sum(n22,n4) = n0
& sum(n22,n3) = n25
& sum(n22,n2) = n24
& sum(n22,n1) = n23
& sum(n22,n0) = n22
& sum(n21,n25) = n20
& sum(n21,n24) = n19
& sum(n21,n23) = n18
& sum(n21,n22) = n17
& sum(n21,n21) = n16
& sum(n21,n20) = n15
& sum(n21,n19) = n14
& sum(n21,n18) = n13
& sum(n21,n17) = n12
& sum(n21,n16) = n11
& sum(n21,n15) = n10
& sum(n21,n14) = n9
& sum(n21,n13) = n8
& sum(n21,n12) = n7
& sum(n21,n11) = n6
& sum(n21,n10) = n5
& sum(n21,n9) = n4
& sum(n21,n8) = n3
& sum(n21,n7) = n2
& sum(n21,n6) = n1
& sum(n21,n5) = n0
& sum(n21,n4) = n25
& sum(n21,n3) = n24
& sum(n21,n2) = n23
& sum(n21,n1) = n22
& sum(n21,n0) = n21
& sum(n20,n25) = n19
& sum(n20,n24) = n18
& sum(n20,n23) = n17
& sum(n20,n22) = n16
& sum(n20,n21) = n15
& sum(n20,n20) = n14
& sum(n20,n19) = n13
& sum(n20,n18) = n12
& sum(n20,n17) = n11
& sum(n20,n16) = n10
& sum(n20,n15) = n9
& sum(n20,n14) = n8
& sum(n20,n13) = n7
& sum(n20,n12) = n6
& sum(n20,n11) = n5
& sum(n20,n10) = n4
& sum(n20,n9) = n3
& sum(n20,n8) = n2
& sum(n20,n7) = n1
& sum(n20,n6) = n0
& sum(n20,n5) = n25
& sum(n20,n4) = n24
& sum(n20,n3) = n23
& sum(n20,n2) = n22
& sum(n20,n1) = n21
& sum(n20,n0) = n20
& sum(n19,n25) = n18
& sum(n19,n24) = n17
& sum(n19,n23) = n16
& sum(n19,n22) = n15
& sum(n19,n21) = n14
& sum(n19,n20) = n13
& sum(n19,n19) = n12
& sum(n19,n18) = n11
& sum(n19,n17) = n10
& sum(n19,n16) = n9
& sum(n19,n15) = n8
& sum(n19,n14) = n7
& sum(n19,n13) = n6
& sum(n19,n12) = n5
& sum(n19,n11) = n4
& sum(n19,n10) = n3
& sum(n19,n9) = n2
& sum(n19,n8) = n1
& sum(n19,n7) = n0
& sum(n19,n6) = n25
& sum(n19,n5) = n24
& sum(n19,n4) = n23
& sum(n19,n3) = n22
& sum(n19,n2) = n21
& sum(n19,n1) = n20
& sum(n19,n0) = n19
& sum(n18,n25) = n17
& sum(n18,n24) = n16
& sum(n18,n23) = n15
& sum(n18,n22) = n14
& sum(n18,n21) = n13
& sum(n18,n20) = n12
& sum(n18,n19) = n11
& sum(n18,n18) = n10
& sum(n18,n17) = n9
& sum(n18,n16) = n8
& sum(n18,n15) = n7
& sum(n18,n14) = n6
& sum(n18,n13) = n5
& sum(n18,n12) = n4
& sum(n18,n11) = n3
& sum(n18,n10) = n2
& sum(n18,n9) = n1
& sum(n18,n8) = n0
& sum(n18,n7) = n25
& sum(n18,n6) = n24
& sum(n18,n5) = n23
& sum(n18,n4) = n22
& sum(n18,n3) = n21
& sum(n18,n2) = n20
& sum(n18,n1) = n19
& sum(n18,n0) = n18
& sum(n17,n25) = n16
& sum(n17,n24) = n15
& sum(n17,n23) = n14
& sum(n17,n22) = n13
& sum(n17,n21) = n12
& sum(n17,n20) = n11
& sum(n17,n19) = n10
& sum(n17,n18) = n9
& sum(n17,n17) = n8
& sum(n17,n16) = n7
& sum(n17,n15) = n6
& sum(n17,n14) = n5
& sum(n17,n13) = n4
& sum(n17,n12) = n3
& sum(n17,n11) = n2
& sum(n17,n10) = n1
& sum(n17,n9) = n0
& sum(n17,n8) = n25
& sum(n17,n7) = n24
& sum(n17,n6) = n23
& sum(n17,n5) = n22
& sum(n17,n4) = n21
& sum(n17,n3) = n20
& sum(n17,n2) = n19
& sum(n17,n1) = n18
& sum(n17,n0) = n17
& sum(n16,n25) = n15
& sum(n16,n24) = n14
& sum(n16,n23) = n13
& sum(n16,n22) = n12
& sum(n16,n21) = n11
& sum(n16,n20) = n10
& sum(n16,n19) = n9
& sum(n16,n18) = n8
& sum(n16,n17) = n7
& sum(n16,n16) = n6
& sum(n16,n15) = n5
& sum(n16,n14) = n4
& sum(n16,n13) = n3
& sum(n16,n12) = n2
& sum(n16,n11) = n1
& sum(n16,n10) = n0
& sum(n16,n9) = n25
& sum(n16,n8) = n24
& sum(n16,n7) = n23
& sum(n16,n6) = n22
& sum(n16,n5) = n21
& sum(n16,n4) = n20
& sum(n16,n3) = n19
& sum(n16,n2) = n18
& sum(n16,n1) = n17
& sum(n16,n0) = n16
& sum(n15,n25) = n14
& sum(n15,n24) = n13
& sum(n15,n23) = n12
& sum(n15,n22) = n11
& sum(n15,n21) = n10
& sum(n15,n20) = n9
& sum(n15,n19) = n8
& sum(n15,n18) = n7
& sum(n15,n17) = n6
& sum(n15,n16) = n5
& sum(n15,n15) = n4
& sum(n15,n14) = n3
& sum(n15,n13) = n2
& sum(n15,n12) = n1
& sum(n15,n11) = n0
& sum(n15,n10) = n25
& sum(n15,n9) = n24
& sum(n15,n8) = n23
& sum(n15,n7) = n22
& sum(n15,n6) = n21
& sum(n15,n5) = n20
& sum(n15,n4) = n19
& sum(n15,n3) = n18
& sum(n15,n2) = n17
& sum(n15,n1) = n16
& sum(n15,n0) = n15
& sum(n14,n25) = n13
& sum(n14,n24) = n12
& sum(n14,n23) = n11
& sum(n14,n22) = n10
& sum(n14,n21) = n9
& sum(n14,n20) = n8
& sum(n14,n19) = n7
& sum(n14,n18) = n6
& sum(n14,n17) = n5
& sum(n14,n16) = n4
& sum(n14,n15) = n3
& sum(n14,n14) = n2
& sum(n14,n13) = n1
& sum(n14,n12) = n0
& sum(n14,n11) = n25
& sum(n14,n10) = n24
& sum(n14,n9) = n23
& sum(n14,n8) = n22
& sum(n14,n7) = n21
& sum(n14,n6) = n20
& sum(n14,n5) = n19
& sum(n14,n4) = n18
& sum(n14,n3) = n17
& sum(n14,n2) = n16
& sum(n14,n1) = n15
& sum(n14,n0) = n14
& sum(n13,n25) = n12
& sum(n13,n24) = n11
& sum(n13,n23) = n10
& sum(n13,n22) = n9
& sum(n13,n21) = n8
& sum(n13,n20) = n7
& sum(n13,n19) = n6
& sum(n13,n18) = n5
& sum(n13,n17) = n4
& sum(n13,n16) = n3
& sum(n13,n15) = n2
& sum(n13,n14) = n1
& sum(n13,n13) = n0
& sum(n13,n12) = n25
& sum(n13,n11) = n24
& sum(n13,n10) = n23
& sum(n13,n9) = n22
& sum(n13,n8) = n21
& sum(n13,n7) = n20
& sum(n13,n6) = n19
& sum(n13,n5) = n18
& sum(n13,n4) = n17
& sum(n13,n3) = n16
& sum(n13,n2) = n15
& sum(n13,n1) = n14
& sum(n13,n0) = n13
& sum(n12,n25) = n11
& sum(n12,n24) = n10
& sum(n12,n23) = n9
& sum(n12,n22) = n8
& sum(n12,n21) = n7
& sum(n12,n20) = n6
& sum(n12,n19) = n5
& sum(n12,n18) = n4
& sum(n12,n17) = n3
& sum(n12,n16) = n2
& sum(n12,n15) = n1
& sum(n12,n14) = n0
& sum(n12,n13) = n25
& sum(n12,n12) = n24
& sum(n12,n11) = n23
& sum(n12,n10) = n22
& sum(n12,n9) = n21
& sum(n12,n8) = n20
& sum(n12,n7) = n19
& sum(n12,n6) = n18
& sum(n12,n5) = n17
& sum(n12,n4) = n16
& sum(n12,n3) = n15
& sum(n12,n2) = n14
& sum(n12,n1) = n13
& sum(n12,n0) = n12
& sum(n11,n25) = n10
& sum(n11,n24) = n9
& sum(n11,n23) = n8
& sum(n11,n22) = n7
& sum(n11,n21) = n6
& sum(n11,n20) = n5
& sum(n11,n19) = n4
& sum(n11,n18) = n3
& sum(n11,n17) = n2
& sum(n11,n16) = n1
& sum(n11,n15) = n0
& sum(n11,n14) = n25
& sum(n11,n13) = n24
& sum(n11,n12) = n23
& sum(n11,n11) = n22
& sum(n11,n10) = n21
& sum(n11,n9) = n20
& sum(n11,n8) = n19
& sum(n11,n7) = n18
& sum(n11,n6) = n17
& sum(n11,n5) = n16
& sum(n11,n4) = n15
& sum(n11,n3) = n14
& sum(n11,n2) = n13
& sum(n11,n1) = n12
& sum(n11,n0) = n11
& sum(n10,n25) = n9
& sum(n10,n24) = n8
& sum(n10,n23) = n7
& sum(n10,n22) = n6
& sum(n10,n21) = n5
& sum(n10,n20) = n4
& sum(n10,n19) = n3
& sum(n10,n18) = n2
& sum(n10,n17) = n1
& sum(n10,n16) = n0
& sum(n10,n15) = n25
& sum(n10,n14) = n24
& sum(n10,n13) = n23
& sum(n10,n12) = n22
& sum(n10,n11) = n21
& sum(n10,n10) = n20
& sum(n10,n9) = n19
& sum(n10,n8) = n18
& sum(n10,n7) = n17
& sum(n10,n6) = n16
& sum(n10,n5) = n15
& sum(n10,n4) = n14
& sum(n10,n3) = n13
& sum(n10,n2) = n12
& sum(n10,n1) = n11
& sum(n10,n0) = n10
& sum(n9,n25) = n8
& sum(n9,n24) = n7
& sum(n9,n23) = n6
& sum(n9,n22) = n5
& sum(n9,n21) = n4
& sum(n9,n20) = n3
& sum(n9,n19) = n2
& sum(n9,n18) = n1
& sum(n9,n17) = n0
& sum(n9,n16) = n25
& sum(n9,n15) = n24
& sum(n9,n14) = n23
& sum(n9,n13) = n22
& sum(n9,n12) = n21
& sum(n9,n11) = n20
& sum(n9,n10) = n19
& sum(n9,n9) = n18
& sum(n9,n8) = n17
& sum(n9,n7) = n16
& sum(n9,n6) = n15
& sum(n9,n5) = n14
& sum(n9,n4) = n13
& sum(n9,n3) = n12
& sum(n9,n2) = n11
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n25) = n7
& sum(n8,n24) = n6
& sum(n8,n23) = n5
& sum(n8,n22) = n4
& sum(n8,n21) = n3
& sum(n8,n20) = n2
& sum(n8,n19) = n1
& sum(n8,n18) = n0
& sum(n8,n17) = n25
& sum(n8,n16) = n24
& sum(n8,n15) = n23
& sum(n8,n14) = n22
& sum(n8,n13) = n21
& sum(n8,n12) = n20
& sum(n8,n11) = n19
& sum(n8,n10) = n18
& sum(n8,n9) = n17
& sum(n8,n8) = n16
& sum(n8,n7) = n15
& sum(n8,n6) = n14
& sum(n8,n5) = n13
& sum(n8,n4) = n12
& sum(n8,n3) = n11
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n25) = n6
& sum(n7,n24) = n5
& sum(n7,n23) = n4
& sum(n7,n22) = n3
& sum(n7,n21) = n2
& sum(n7,n20) = n1
& sum(n7,n19) = n0
& sum(n7,n18) = n25
& sum(n7,n17) = n24
& sum(n7,n16) = n23
& sum(n7,n15) = n22
& sum(n7,n14) = n21
& sum(n7,n13) = n20
& sum(n7,n12) = n19
& sum(n7,n11) = n18
& sum(n7,n10) = n17
& sum(n7,n9) = n16
& sum(n7,n8) = n15
& sum(n7,n7) = n14
& sum(n7,n6) = n13
& sum(n7,n5) = n12
& sum(n7,n4) = n11
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n25) = n5
& sum(n6,n24) = n4
& sum(n6,n23) = n3
& sum(n6,n22) = n2
& sum(n6,n21) = n1
& sum(n6,n20) = n0
& sum(n6,n19) = n25
& sum(n6,n18) = n24
& sum(n6,n17) = n23
& sum(n6,n16) = n22
& sum(n6,n15) = n21
& sum(n6,n14) = n20
& sum(n6,n13) = n19
& sum(n6,n12) = n18
& sum(n6,n11) = n17
& sum(n6,n10) = n16
& sum(n6,n9) = n15
& sum(n6,n8) = n14
& sum(n6,n7) = n13
& sum(n6,n6) = n12
& sum(n6,n5) = n11
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n25) = n4
& sum(n5,n24) = n3
& sum(n5,n23) = n2
& sum(n5,n22) = n1
& sum(n5,n21) = n0
& sum(n5,n20) = n25
& sum(n5,n19) = n24
& sum(n5,n18) = n23
& sum(n5,n17) = n22
& sum(n5,n16) = n21
& sum(n5,n15) = n20
& sum(n5,n14) = n19
& sum(n5,n13) = n18
& sum(n5,n12) = n17
& sum(n5,n11) = n16
& sum(n5,n10) = n15
& sum(n5,n9) = n14
& sum(n5,n8) = n13
& sum(n5,n7) = n12
& sum(n5,n6) = n11
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n25) = n3
& sum(n4,n24) = n2
& sum(n4,n23) = n1
& sum(n4,n22) = n0
& sum(n4,n21) = n25
& sum(n4,n20) = n24
& sum(n4,n19) = n23
& sum(n4,n18) = n22
& sum(n4,n17) = n21
& sum(n4,n16) = n20
& sum(n4,n15) = n19
& sum(n4,n14) = n18
& sum(n4,n13) = n17
& sum(n4,n12) = n16
& sum(n4,n11) = n15
& sum(n4,n10) = n14
& sum(n4,n9) = n13
& sum(n4,n8) = n12
& sum(n4,n7) = n11
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n25) = n2
& sum(n3,n24) = n1
& sum(n3,n23) = n0
& sum(n3,n22) = n25
& sum(n3,n21) = n24
& sum(n3,n20) = n23
& sum(n3,n19) = n22
& sum(n3,n18) = n21
& sum(n3,n17) = n20
& sum(n3,n16) = n19
& sum(n3,n15) = n18
& sum(n3,n14) = n17
& sum(n3,n13) = n16
& sum(n3,n12) = n15
& sum(n3,n11) = n14
& sum(n3,n10) = n13
& sum(n3,n9) = n12
& sum(n3,n8) = n11
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n25) = n1
& sum(n2,n24) = n0
& sum(n2,n23) = n25
& sum(n2,n22) = n24
& sum(n2,n21) = n23
& sum(n2,n20) = n22
& sum(n2,n19) = n21
& sum(n2,n18) = n20
& sum(n2,n17) = n19
& sum(n2,n16) = n18
& sum(n2,n15) = n17
& sum(n2,n14) = n16
& sum(n2,n13) = n15
& sum(n2,n12) = n14
& sum(n2,n11) = n13
& sum(n2,n10) = n12
& sum(n2,n9) = n11
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n25) = n0
& sum(n1,n24) = n25
& sum(n1,n23) = n24
& sum(n1,n22) = n23
& sum(n1,n21) = n22
& sum(n1,n20) = n21
& sum(n1,n19) = n20
& sum(n1,n18) = n19
& sum(n1,n17) = n18
& sum(n1,n16) = n17
& sum(n1,n15) = n16
& sum(n1,n14) = n15
& sum(n1,n13) = n14
& sum(n1,n12) = n13
& sum(n1,n11) = n12
& sum(n1,n10) = n11
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n25) = n25
& sum(n0,n24) = n24
& sum(n0,n23) = n23
& sum(n0,n22) = n22
& sum(n0,n21) = n21
& sum(n0,n20) = n20
& sum(n0,n19) = n19
& sum(n0,n18) = n18
& sum(n0,n17) = n17
& sum(n0,n16) = n16
& sum(n0,n15) = n15
& sum(n0,n14) = n14
& sum(n0,n13) = n13
& sum(n0,n12) = n12
& sum(n0,n11) = n11
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n25) = n24
& pred(n24) = n23
& pred(n23) = n22
& pred(n22) = n21
& pred(n21) = n20
& pred(n20) = n19
& pred(n19) = n18
& pred(n18) = n17
& pred(n17) = n16
& pred(n16) = n15
& pred(n15) = n14
& pred(n14) = n13
& pred(n13) = n12
& pred(n12) = n11
& pred(n11) = n10
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n25
& succ(n25) = n0
& succ(n24) = n25
& succ(n23) = n24
& succ(n22) = n23
& succ(n21) = n22
& succ(n20) = n21
& succ(n19) = n20
& succ(n18) = n19
& succ(n17) = n18
& succ(n16) = n17
& succ(n15) = n16
& succ(n14) = n15
& succ(n13) = n14
& succ(n12) = n13
& succ(n11) = n12
& succ(n10) = n11
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
& succ(n0) = n1 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( n24 != n25
& n23 != n25
& n23 != n24
& n22 != n25
& n22 != n24
& n22 != n23
& n21 != n25
& n21 != n24
& n21 != n23
& n21 != n22
& n20 != n25
& n20 != n24
& n20 != n23
& n20 != n22
& n20 != n21
& n19 != n25
& n19 != n24
& n19 != n23
& n19 != n22
& n19 != n21
& n19 != n20
& n18 != n25
& n18 != n24
& n18 != n23
& n18 != n22
& n18 != n21
& n18 != n20
& n18 != n19
& n17 != n25
& n17 != n24
& n17 != n23
& n17 != n22
& n17 != n21
& n17 != n20
& n17 != n19
& n17 != n18
& n16 != n25
& n16 != n24
& n16 != n23
& n16 != n22
& n16 != n21
& n16 != n20
& n16 != n19
& n16 != n18
& n16 != n17
& n15 != n25
& n15 != n24
& n15 != n23
& n15 != n22
& n15 != n21
& n15 != n20
& n15 != n19
& n15 != n18
& n15 != n17
& n15 != n16
& n14 != n25
& n14 != n24
& n14 != n23
& n14 != n22
& n14 != n21
& n14 != n20
& n14 != n19
& n14 != n18
& n14 != n17
& n14 != n16
& n14 != n15
& n13 != n25
& n13 != n24
& n13 != n23
& n13 != n22
& n13 != n21
& n13 != n20
& n13 != n19
& n13 != n18
& n13 != n17
& n13 != n16
& n13 != n15
& n13 != n14
& n12 != n25
& n12 != n24
& n12 != n23
& n12 != n22
& n12 != n21
& n12 != n20
& n12 != n19
& n12 != n18
& n12 != n17
& n12 != n16
& n12 != n15
& n12 != n14
& n12 != n13
& n11 != n25
& n11 != n24
& n11 != n23
& n11 != n22
& n11 != n21
& n11 != n20
& n11 != n19
& n11 != n18
& n11 != n17
& n11 != n16
& n11 != n15
& n11 != n14
& n11 != n13
& n11 != n12
& n10 != n25
& n10 != n24
& n10 != n23
& n10 != n22
& n10 != n21
& n10 != n20
& n10 != n19
& n10 != n18
& n10 != n17
& n10 != n16
& n10 != n15
& n10 != n14
& n10 != n13
& n10 != n12
& n10 != n11
& n9 != n25
& n9 != n24
& n9 != n23
& n9 != n22
& n9 != n21
& n9 != n20
& n9 != n19
& n9 != n18
& n9 != n17
& n9 != n16
& n9 != n15
& n9 != n14
& n9 != n13
& n9 != n12
& n9 != n11
& n9 != n10
& n8 != n25
& n8 != n24
& n8 != n23
& n8 != n22
& n8 != n21
& n8 != n20
& n8 != n19
& n8 != n18
& n8 != n17
& n8 != n16
& n8 != n15
& n8 != n14
& n8 != n13
& n8 != n12
& n8 != n11
& n8 != n10
& n8 != n9
& n7 != n25
& n7 != n24
& n7 != n23
& n7 != n22
& n7 != n21
& n7 != n20
& n7 != n19
& n7 != n18
& n7 != n17
& n7 != n16
& n7 != n15
& n7 != n14
& n7 != n13
& n7 != n12
& n7 != n11
& n7 != n10
& n7 != n9
& n7 != n8
& n6 != n25
& n6 != n24
& n6 != n23
& n6 != n22
& n6 != n21
& n6 != n20
& n6 != n19
& n6 != n18
& n6 != n17
& n6 != n16
& n6 != n15
& n6 != n14
& n6 != n13
& n6 != n12
& n6 != n11
& n6 != n10
& n6 != n9
& n6 != n8
& n6 != n7
& n5 != n25
& n5 != n24
& n5 != n23
& n5 != n22
& n5 != n21
& n5 != n20
& n5 != n19
& n5 != n18
& n5 != n17
& n5 != n16
& n5 != n15
& n5 != n14
& n5 != n13
& n5 != n12
& n5 != n11
& n5 != n10
& n5 != n9
& n5 != n8
& n5 != n7
& n5 != n6
& n4 != n25
& n4 != n24
& n4 != n23
& n4 != n22
& n4 != n21
& n4 != n20
& n4 != n19
& n4 != n18
& n4 != n17
& n4 != n16
& n4 != n15
& n4 != n14
& n4 != n13
& n4 != n12
& n4 != n11
& n4 != n10
& n4 != n9
& n4 != n8
& n4 != n7
& n4 != n6
& n4 != n5
& n3 != n25
& n3 != n24
& n3 != n23
& n3 != n22
& n3 != n21
& n3 != n20
& n3 != n19
& n3 != n18
& n3 != n17
& n3 != n16
& n3 != n15
& n3 != n14
& n3 != n13
& n3 != n12
& n3 != n11
& n3 != n10
& n3 != n9
& n3 != n8
& n3 != n7
& n3 != n6
& n3 != n5
& n3 != n4
& n2 != n25
& n2 != n24
& n2 != n23
& n2 != n22
& n2 != n21
& n2 != n20
& n2 != n19
& n2 != n18
& n2 != n17
& n2 != n16
& n2 != n15
& n2 != n14
& n2 != n13
& n2 != n12
& n2 != n11
& n2 != n10
& n2 != n9
& n2 != n8
& n2 != n7
& n2 != n6
& n2 != n5
& n2 != n4
& n2 != n3
& n1 != n25
& n1 != n24
& n1 != n23
& n1 != n22
& n1 != n21
& n1 != n20
& n1 != n19
& n1 != n18
& n1 != n17
& n1 != n16
& n1 != n15
& n1 != n14
& n1 != n13
& n1 != n12
& n1 != n11
& n1 != n10
& n1 != n9
& n1 != n8
& n1 != n7
& n1 != n6
& n1 != n5
& n1 != n4
& n1 != n3
& n1 != n2
& n0 != n25
& n0 != n24
& n0 != n23
& n0 != n22
& n0 != n21
& n0 != n20
& n0 != n19
& n0 != n18
& n0 != n17
& n0 != n16
& n0 != n15
& n0 != n14
& n0 != n13
& n0 != n12
& n0 != n11
& n0 != n10
& n0 != n9
& n0 != n8
& n0 != n7
& n0 != n6
& n0 != n5
& n0 != n4
& n0 != n3
& n0 != n2
& n0 != n1
& sk2 != n25
& sk2 != n24
& sk2 != n23
& sk2 != n22
& sk2 != n21
& sk2 != n20
& sk2 != n19
& sk2 != n18
& sk2 != n17
& sk2 != n16
& sk2 != n15
& sk2 != n14
& sk2 != n13
& sk2 != n12
& sk2 != n11
& sk2 != n10
& sk2 != n9
& sk2 != n8
& sk2 != n7
& sk2 != n6
& sk2 != n5
& sk2 != n4
& sk2 != n3
& sk2 != n2
& sk2 != n1
& sk2 != n0
& sk2 = sum(pred(sum(sk0,succ(sk1))),sum(sk1,pred(sum(sk0,sk1))))
& ( sk1 = n25
| sk1 = n24
| sk1 = n23
| sk1 = n22
| sk1 = n21
| sk1 = n20
| sk1 = n19
| sk1 = n18
| sk1 = n17
| sk1 = n16
| sk1 = n15
| sk1 = n14
| sk1 = n13
| sk1 = n12
| sk1 = n11
| sk1 = n10
| sk1 = n9
| sk1 = n8
| sk1 = n7
| sk1 = n6
| sk1 = n5
| sk1 = n4
| sk1 = n3
| sk1 = n2
| sk1 = n1
| sk1 = n0 )
& ( sk0 = n25
| sk0 = n24
| sk0 = n23
| sk0 = n22
| sk0 = n21
| sk0 = n20
| sk0 = n19
| sk0 = n18
| sk0 = n17
| sk0 = n16
| sk0 = n15
| sk0 = n14
| sk0 = n13
| sk0 = n12
| sk0 = n11
| sk0 = n10
| sk0 = n9
| sk0 = n8
| sk0 = n7
| sk0 = n6
| sk0 = n5
| sk0 = n4
| sk0 = n3
| sk0 = n2
| sk0 = n1
| sk0 = n0 )
& sum(n25,n25) = n24
& sum(n25,n24) = n23
& sum(n25,n23) = n22
& sum(n25,n22) = n21
& sum(n25,n21) = n20
& sum(n25,n20) = n19
& sum(n25,n19) = n18
& sum(n25,n18) = n17
& sum(n25,n17) = n16
& sum(n25,n16) = n15
& sum(n25,n15) = n14
& sum(n25,n14) = n13
& sum(n25,n13) = n12
& sum(n25,n12) = n11
& sum(n25,n11) = n10
& sum(n25,n10) = n9
& sum(n25,n9) = n8
& sum(n25,n8) = n7
& sum(n25,n7) = n6
& sum(n25,n6) = n5
& sum(n25,n5) = n4
& sum(n25,n4) = n3
& sum(n25,n3) = n2
& sum(n25,n2) = n1
& sum(n25,n1) = n0
& sum(n25,n0) = n25
& sum(n24,n25) = n23
& sum(n24,n24) = n22
& sum(n24,n23) = n21
& sum(n24,n22) = n20
& sum(n24,n21) = n19
& sum(n24,n20) = n18
& sum(n24,n19) = n17
& sum(n24,n18) = n16
& sum(n24,n17) = n15
& sum(n24,n16) = n14
& sum(n24,n15) = n13
& sum(n24,n14) = n12
& sum(n24,n13) = n11
& sum(n24,n12) = n10
& sum(n24,n11) = n9
& sum(n24,n10) = n8
& sum(n24,n9) = n7
& sum(n24,n8) = n6
& sum(n24,n7) = n5
& sum(n24,n6) = n4
& sum(n24,n5) = n3
& sum(n24,n4) = n2
& sum(n24,n3) = n1
& sum(n24,n2) = n0
& sum(n24,n1) = n25
& sum(n24,n0) = n24
& sum(n23,n25) = n22
& sum(n23,n24) = n21
& sum(n23,n23) = n20
& sum(n23,n22) = n19
& sum(n23,n21) = n18
& sum(n23,n20) = n17
& sum(n23,n19) = n16
& sum(n23,n18) = n15
& sum(n23,n17) = n14
& sum(n23,n16) = n13
& sum(n23,n15) = n12
& sum(n23,n14) = n11
& sum(n23,n13) = n10
& sum(n23,n12) = n9
& sum(n23,n11) = n8
& sum(n23,n10) = n7
& sum(n23,n9) = n6
& sum(n23,n8) = n5
& sum(n23,n7) = n4
& sum(n23,n6) = n3
& sum(n23,n5) = n2
& sum(n23,n4) = n1
& sum(n23,n3) = n0
& sum(n23,n2) = n25
& sum(n23,n1) = n24
& sum(n23,n0) = n23
& sum(n22,n25) = n21
& sum(n22,n24) = n20
& sum(n22,n23) = n19
& sum(n22,n22) = n18
& sum(n22,n21) = n17
& sum(n22,n20) = n16
& sum(n22,n19) = n15
& sum(n22,n18) = n14
& sum(n22,n17) = n13
& sum(n22,n16) = n12
& sum(n22,n15) = n11
& sum(n22,n14) = n10
& sum(n22,n13) = n9
& sum(n22,n12) = n8
& sum(n22,n11) = n7
& sum(n22,n10) = n6
& sum(n22,n9) = n5
& sum(n22,n8) = n4
& sum(n22,n7) = n3
& sum(n22,n6) = n2
& sum(n22,n5) = n1
& sum(n22,n4) = n0
& sum(n22,n3) = n25
& sum(n22,n2) = n24
& sum(n22,n1) = n23
& sum(n22,n0) = n22
& sum(n21,n25) = n20
& sum(n21,n24) = n19
& sum(n21,n23) = n18
& sum(n21,n22) = n17
& sum(n21,n21) = n16
& sum(n21,n20) = n15
& sum(n21,n19) = n14
& sum(n21,n18) = n13
& sum(n21,n17) = n12
& sum(n21,n16) = n11
& sum(n21,n15) = n10
& sum(n21,n14) = n9
& sum(n21,n13) = n8
& sum(n21,n12) = n7
& sum(n21,n11) = n6
& sum(n21,n10) = n5
& sum(n21,n9) = n4
& sum(n21,n8) = n3
& sum(n21,n7) = n2
& sum(n21,n6) = n1
& sum(n21,n5) = n0
& sum(n21,n4) = n25
& sum(n21,n3) = n24
& sum(n21,n2) = n23
& sum(n21,n1) = n22
& sum(n21,n0) = n21
& sum(n20,n25) = n19
& sum(n20,n24) = n18
& sum(n20,n23) = n17
& sum(n20,n22) = n16
& sum(n20,n21) = n15
& sum(n20,n20) = n14
& sum(n20,n19) = n13
& sum(n20,n18) = n12
& sum(n20,n17) = n11
& sum(n20,n16) = n10
& sum(n20,n15) = n9
& sum(n20,n14) = n8
& sum(n20,n13) = n7
& sum(n20,n12) = n6
& sum(n20,n11) = n5
& sum(n20,n10) = n4
& sum(n20,n9) = n3
& sum(n20,n8) = n2
& sum(n20,n7) = n1
& sum(n20,n6) = n0
& sum(n20,n5) = n25
& sum(n20,n4) = n24
& sum(n20,n3) = n23
& sum(n20,n2) = n22
& sum(n20,n1) = n21
& sum(n20,n0) = n20
& sum(n19,n25) = n18
& sum(n19,n24) = n17
& sum(n19,n23) = n16
& sum(n19,n22) = n15
& sum(n19,n21) = n14
& sum(n19,n20) = n13
& sum(n19,n19) = n12
& sum(n19,n18) = n11
& sum(n19,n17) = n10
& sum(n19,n16) = n9
& sum(n19,n15) = n8
& sum(n19,n14) = n7
& sum(n19,n13) = n6
& sum(n19,n12) = n5
& sum(n19,n11) = n4
& sum(n19,n10) = n3
& sum(n19,n9) = n2
& sum(n19,n8) = n1
& sum(n19,n7) = n0
& sum(n19,n6) = n25
& sum(n19,n5) = n24
& sum(n19,n4) = n23
& sum(n19,n3) = n22
& sum(n19,n2) = n21
& sum(n19,n1) = n20
& sum(n19,n0) = n19
& sum(n18,n25) = n17
& sum(n18,n24) = n16
& sum(n18,n23) = n15
& sum(n18,n22) = n14
& sum(n18,n21) = n13
& sum(n18,n20) = n12
& sum(n18,n19) = n11
& sum(n18,n18) = n10
& sum(n18,n17) = n9
& sum(n18,n16) = n8
& sum(n18,n15) = n7
& sum(n18,n14) = n6
& sum(n18,n13) = n5
& sum(n18,n12) = n4
& sum(n18,n11) = n3
& sum(n18,n10) = n2
& sum(n18,n9) = n1
& sum(n18,n8) = n0
& sum(n18,n7) = n25
& sum(n18,n6) = n24
& sum(n18,n5) = n23
& sum(n18,n4) = n22
& sum(n18,n3) = n21
& sum(n18,n2) = n20
& sum(n18,n1) = n19
& sum(n18,n0) = n18
& sum(n17,n25) = n16
& sum(n17,n24) = n15
& sum(n17,n23) = n14
& sum(n17,n22) = n13
& sum(n17,n21) = n12
& sum(n17,n20) = n11
& sum(n17,n19) = n10
& sum(n17,n18) = n9
& sum(n17,n17) = n8
& sum(n17,n16) = n7
& sum(n17,n15) = n6
& sum(n17,n14) = n5
& sum(n17,n13) = n4
& sum(n17,n12) = n3
& sum(n17,n11) = n2
& sum(n17,n10) = n1
& sum(n17,n9) = n0
& sum(n17,n8) = n25
& sum(n17,n7) = n24
& sum(n17,n6) = n23
& sum(n17,n5) = n22
& sum(n17,n4) = n21
& sum(n17,n3) = n20
& sum(n17,n2) = n19
& sum(n17,n1) = n18
& sum(n17,n0) = n17
& sum(n16,n25) = n15
& sum(n16,n24) = n14
& sum(n16,n23) = n13
& sum(n16,n22) = n12
& sum(n16,n21) = n11
& sum(n16,n20) = n10
& sum(n16,n19) = n9
& sum(n16,n18) = n8
& sum(n16,n17) = n7
& sum(n16,n16) = n6
& sum(n16,n15) = n5
& sum(n16,n14) = n4
& sum(n16,n13) = n3
& sum(n16,n12) = n2
& sum(n16,n11) = n1
& sum(n16,n10) = n0
& sum(n16,n9) = n25
& sum(n16,n8) = n24
& sum(n16,n7) = n23
& sum(n16,n6) = n22
& sum(n16,n5) = n21
& sum(n16,n4) = n20
& sum(n16,n3) = n19
& sum(n16,n2) = n18
& sum(n16,n1) = n17
& sum(n16,n0) = n16
& sum(n15,n25) = n14
& sum(n15,n24) = n13
& sum(n15,n23) = n12
& sum(n15,n22) = n11
& sum(n15,n21) = n10
& sum(n15,n20) = n9
& sum(n15,n19) = n8
& sum(n15,n18) = n7
& sum(n15,n17) = n6
& sum(n15,n16) = n5
& sum(n15,n15) = n4
& sum(n15,n14) = n3
& sum(n15,n13) = n2
& sum(n15,n12) = n1
& sum(n15,n11) = n0
& sum(n15,n10) = n25
& sum(n15,n9) = n24
& sum(n15,n8) = n23
& sum(n15,n7) = n22
& sum(n15,n6) = n21
& sum(n15,n5) = n20
& sum(n15,n4) = n19
& sum(n15,n3) = n18
& sum(n15,n2) = n17
& sum(n15,n1) = n16
& sum(n15,n0) = n15
& sum(n14,n25) = n13
& sum(n14,n24) = n12
& sum(n14,n23) = n11
& sum(n14,n22) = n10
& sum(n14,n21) = n9
& sum(n14,n20) = n8
& sum(n14,n19) = n7
& sum(n14,n18) = n6
& sum(n14,n17) = n5
& sum(n14,n16) = n4
& sum(n14,n15) = n3
& sum(n14,n14) = n2
& sum(n14,n13) = n1
& sum(n14,n12) = n0
& sum(n14,n11) = n25
& sum(n14,n10) = n24
& sum(n14,n9) = n23
& sum(n14,n8) = n22
& sum(n14,n7) = n21
& sum(n14,n6) = n20
& sum(n14,n5) = n19
& sum(n14,n4) = n18
& sum(n14,n3) = n17
& sum(n14,n2) = n16
& sum(n14,n1) = n15
& sum(n14,n0) = n14
& sum(n13,n25) = n12
& sum(n13,n24) = n11
& sum(n13,n23) = n10
& sum(n13,n22) = n9
& sum(n13,n21) = n8
& sum(n13,n20) = n7
& sum(n13,n19) = n6
& sum(n13,n18) = n5
& sum(n13,n17) = n4
& sum(n13,n16) = n3
& sum(n13,n15) = n2
& sum(n13,n14) = n1
& sum(n13,n13) = n0
& sum(n13,n12) = n25
& sum(n13,n11) = n24
& sum(n13,n10) = n23
& sum(n13,n9) = n22
& sum(n13,n8) = n21
& sum(n13,n7) = n20
& sum(n13,n6) = n19
& sum(n13,n5) = n18
& sum(n13,n4) = n17
& sum(n13,n3) = n16
& sum(n13,n2) = n15
& sum(n13,n1) = n14
& sum(n13,n0) = n13
& sum(n12,n25) = n11
& sum(n12,n24) = n10
& sum(n12,n23) = n9
& sum(n12,n22) = n8
& sum(n12,n21) = n7
& sum(n12,n20) = n6
& sum(n12,n19) = n5
& sum(n12,n18) = n4
& sum(n12,n17) = n3
& sum(n12,n16) = n2
& sum(n12,n15) = n1
& sum(n12,n14) = n0
& sum(n12,n13) = n25
& sum(n12,n12) = n24
& sum(n12,n11) = n23
& sum(n12,n10) = n22
& sum(n12,n9) = n21
& sum(n12,n8) = n20
& sum(n12,n7) = n19
& sum(n12,n6) = n18
& sum(n12,n5) = n17
& sum(n12,n4) = n16
& sum(n12,n3) = n15
& sum(n12,n2) = n14
& sum(n12,n1) = n13
& sum(n12,n0) = n12
& sum(n11,n25) = n10
& sum(n11,n24) = n9
& sum(n11,n23) = n8
& sum(n11,n22) = n7
& sum(n11,n21) = n6
& sum(n11,n20) = n5
& sum(n11,n19) = n4
& sum(n11,n18) = n3
& sum(n11,n17) = n2
& sum(n11,n16) = n1
& sum(n11,n15) = n0
& sum(n11,n14) = n25
& sum(n11,n13) = n24
& sum(n11,n12) = n23
& sum(n11,n11) = n22
& sum(n11,n10) = n21
& sum(n11,n9) = n20
& sum(n11,n8) = n19
& sum(n11,n7) = n18
& sum(n11,n6) = n17
& sum(n11,n5) = n16
& sum(n11,n4) = n15
& sum(n11,n3) = n14
& sum(n11,n2) = n13
& sum(n11,n1) = n12
& sum(n11,n0) = n11
& sum(n10,n25) = n9
& sum(n10,n24) = n8
& sum(n10,n23) = n7
& sum(n10,n22) = n6
& sum(n10,n21) = n5
& sum(n10,n20) = n4
& sum(n10,n19) = n3
& sum(n10,n18) = n2
& sum(n10,n17) = n1
& sum(n10,n16) = n0
& sum(n10,n15) = n25
& sum(n10,n14) = n24
& sum(n10,n13) = n23
& sum(n10,n12) = n22
& sum(n10,n11) = n21
& sum(n10,n10) = n20
& sum(n10,n9) = n19
& sum(n10,n8) = n18
& sum(n10,n7) = n17
& sum(n10,n6) = n16
& sum(n10,n5) = n15
& sum(n10,n4) = n14
& sum(n10,n3) = n13
& sum(n10,n2) = n12
& sum(n10,n1) = n11
& sum(n10,n0) = n10
& sum(n9,n25) = n8
& sum(n9,n24) = n7
& sum(n9,n23) = n6
& sum(n9,n22) = n5
& sum(n9,n21) = n4
& sum(n9,n20) = n3
& sum(n9,n19) = n2
& sum(n9,n18) = n1
& sum(n9,n17) = n0
& sum(n9,n16) = n25
& sum(n9,n15) = n24
& sum(n9,n14) = n23
& sum(n9,n13) = n22
& sum(n9,n12) = n21
& sum(n9,n11) = n20
& sum(n9,n10) = n19
& sum(n9,n9) = n18
& sum(n9,n8) = n17
& sum(n9,n7) = n16
& sum(n9,n6) = n15
& sum(n9,n5) = n14
& sum(n9,n4) = n13
& sum(n9,n3) = n12
& sum(n9,n2) = n11
& sum(n9,n1) = n10
& sum(n9,n0) = n9
& sum(n8,n25) = n7
& sum(n8,n24) = n6
& sum(n8,n23) = n5
& sum(n8,n22) = n4
& sum(n8,n21) = n3
& sum(n8,n20) = n2
& sum(n8,n19) = n1
& sum(n8,n18) = n0
& sum(n8,n17) = n25
& sum(n8,n16) = n24
& sum(n8,n15) = n23
& sum(n8,n14) = n22
& sum(n8,n13) = n21
& sum(n8,n12) = n20
& sum(n8,n11) = n19
& sum(n8,n10) = n18
& sum(n8,n9) = n17
& sum(n8,n8) = n16
& sum(n8,n7) = n15
& sum(n8,n6) = n14
& sum(n8,n5) = n13
& sum(n8,n4) = n12
& sum(n8,n3) = n11
& sum(n8,n2) = n10
& sum(n8,n1) = n9
& sum(n8,n0) = n8
& sum(n7,n25) = n6
& sum(n7,n24) = n5
& sum(n7,n23) = n4
& sum(n7,n22) = n3
& sum(n7,n21) = n2
& sum(n7,n20) = n1
& sum(n7,n19) = n0
& sum(n7,n18) = n25
& sum(n7,n17) = n24
& sum(n7,n16) = n23
& sum(n7,n15) = n22
& sum(n7,n14) = n21
& sum(n7,n13) = n20
& sum(n7,n12) = n19
& sum(n7,n11) = n18
& sum(n7,n10) = n17
& sum(n7,n9) = n16
& sum(n7,n8) = n15
& sum(n7,n7) = n14
& sum(n7,n6) = n13
& sum(n7,n5) = n12
& sum(n7,n4) = n11
& sum(n7,n3) = n10
& sum(n7,n2) = n9
& sum(n7,n1) = n8
& sum(n7,n0) = n7
& sum(n6,n25) = n5
& sum(n6,n24) = n4
& sum(n6,n23) = n3
& sum(n6,n22) = n2
& sum(n6,n21) = n1
& sum(n6,n20) = n0
& sum(n6,n19) = n25
& sum(n6,n18) = n24
& sum(n6,n17) = n23
& sum(n6,n16) = n22
& sum(n6,n15) = n21
& sum(n6,n14) = n20
& sum(n6,n13) = n19
& sum(n6,n12) = n18
& sum(n6,n11) = n17
& sum(n6,n10) = n16
& sum(n6,n9) = n15
& sum(n6,n8) = n14
& sum(n6,n7) = n13
& sum(n6,n6) = n12
& sum(n6,n5) = n11
& sum(n6,n4) = n10
& sum(n6,n3) = n9
& sum(n6,n2) = n8
& sum(n6,n1) = n7
& sum(n6,n0) = n6
& sum(n5,n25) = n4
& sum(n5,n24) = n3
& sum(n5,n23) = n2
& sum(n5,n22) = n1
& sum(n5,n21) = n0
& sum(n5,n20) = n25
& sum(n5,n19) = n24
& sum(n5,n18) = n23
& sum(n5,n17) = n22
& sum(n5,n16) = n21
& sum(n5,n15) = n20
& sum(n5,n14) = n19
& sum(n5,n13) = n18
& sum(n5,n12) = n17
& sum(n5,n11) = n16
& sum(n5,n10) = n15
& sum(n5,n9) = n14
& sum(n5,n8) = n13
& sum(n5,n7) = n12
& sum(n5,n6) = n11
& sum(n5,n5) = n10
& sum(n5,n4) = n9
& sum(n5,n3) = n8
& sum(n5,n2) = n7
& sum(n5,n1) = n6
& sum(n5,n0) = n5
& sum(n4,n25) = n3
& sum(n4,n24) = n2
& sum(n4,n23) = n1
& sum(n4,n22) = n0
& sum(n4,n21) = n25
& sum(n4,n20) = n24
& sum(n4,n19) = n23
& sum(n4,n18) = n22
& sum(n4,n17) = n21
& sum(n4,n16) = n20
& sum(n4,n15) = n19
& sum(n4,n14) = n18
& sum(n4,n13) = n17
& sum(n4,n12) = n16
& sum(n4,n11) = n15
& sum(n4,n10) = n14
& sum(n4,n9) = n13
& sum(n4,n8) = n12
& sum(n4,n7) = n11
& sum(n4,n6) = n10
& sum(n4,n5) = n9
& sum(n4,n4) = n8
& sum(n4,n3) = n7
& sum(n4,n2) = n6
& sum(n4,n1) = n5
& sum(n4,n0) = n4
& sum(n3,n25) = n2
& sum(n3,n24) = n1
& sum(n3,n23) = n0
& sum(n3,n22) = n25
& sum(n3,n21) = n24
& sum(n3,n20) = n23
& sum(n3,n19) = n22
& sum(n3,n18) = n21
& sum(n3,n17) = n20
& sum(n3,n16) = n19
& sum(n3,n15) = n18
& sum(n3,n14) = n17
& sum(n3,n13) = n16
& sum(n3,n12) = n15
& sum(n3,n11) = n14
& sum(n3,n10) = n13
& sum(n3,n9) = n12
& sum(n3,n8) = n11
& sum(n3,n7) = n10
& sum(n3,n6) = n9
& sum(n3,n5) = n8
& sum(n3,n4) = n7
& sum(n3,n3) = n6
& sum(n3,n2) = n5
& sum(n3,n1) = n4
& sum(n3,n0) = n3
& sum(n2,n25) = n1
& sum(n2,n24) = n0
& sum(n2,n23) = n25
& sum(n2,n22) = n24
& sum(n2,n21) = n23
& sum(n2,n20) = n22
& sum(n2,n19) = n21
& sum(n2,n18) = n20
& sum(n2,n17) = n19
& sum(n2,n16) = n18
& sum(n2,n15) = n17
& sum(n2,n14) = n16
& sum(n2,n13) = n15
& sum(n2,n12) = n14
& sum(n2,n11) = n13
& sum(n2,n10) = n12
& sum(n2,n9) = n11
& sum(n2,n8) = n10
& sum(n2,n7) = n9
& sum(n2,n6) = n8
& sum(n2,n5) = n7
& sum(n2,n4) = n6
& sum(n2,n3) = n5
& sum(n2,n2) = n4
& sum(n2,n1) = n3
& sum(n2,n0) = n2
& sum(n1,n25) = n0
& sum(n1,n24) = n25
& sum(n1,n23) = n24
& sum(n1,n22) = n23
& sum(n1,n21) = n22
& sum(n1,n20) = n21
& sum(n1,n19) = n20
& sum(n1,n18) = n19
& sum(n1,n17) = n18
& sum(n1,n16) = n17
& sum(n1,n15) = n16
& sum(n1,n14) = n15
& sum(n1,n13) = n14
& sum(n1,n12) = n13
& sum(n1,n11) = n12
& sum(n1,n10) = n11
& sum(n1,n9) = n10
& sum(n1,n8) = n9
& sum(n1,n7) = n8
& sum(n1,n6) = n7
& sum(n1,n5) = n6
& sum(n1,n4) = n5
& sum(n1,n3) = n4
& sum(n1,n2) = n3
& sum(n1,n1) = n2
& sum(n1,n0) = n1
& sum(n0,n25) = n25
& sum(n0,n24) = n24
& sum(n0,n23) = n23
& sum(n0,n22) = n22
& sum(n0,n21) = n21
& sum(n0,n20) = n20
& sum(n0,n19) = n19
& sum(n0,n18) = n18
& sum(n0,n17) = n17
& sum(n0,n16) = n16
& sum(n0,n15) = n15
& sum(n0,n14) = n14
& sum(n0,n13) = n13
& sum(n0,n12) = n12
& sum(n0,n11) = n11
& sum(n0,n10) = n10
& sum(n0,n9) = n9
& sum(n0,n8) = n8
& sum(n0,n7) = n7
& sum(n0,n6) = n6
& sum(n0,n5) = n5
& sum(n0,n4) = n4
& sum(n0,n3) = n3
& sum(n0,n2) = n2
& sum(n0,n1) = n1
& sum(n0,n0) = n0
& pred(n25) = n24
& pred(n24) = n23
& pred(n23) = n22
& pred(n22) = n21
& pred(n21) = n20
& pred(n20) = n19
& pred(n19) = n18
& pred(n18) = n17
& pred(n17) = n16
& pred(n16) = n15
& pred(n15) = n14
& pred(n14) = n13
& pred(n13) = n12
& pred(n12) = n11
& pred(n11) = n10
& pred(n10) = n9
& pred(n9) = n8
& pred(n8) = n7
& pred(n7) = n6
& pred(n6) = n5
& pred(n5) = n4
& pred(n4) = n3
& pred(n3) = n2
& pred(n2) = n1
& pred(n1) = n0
& pred(n0) = n25
& succ(n25) = n0
& succ(n24) = n25
& succ(n23) = n24
& succ(n22) = n23
& succ(n21) = n22
& succ(n20) = n21
& succ(n19) = n20
& succ(n18) = n19
& succ(n17) = n18
& succ(n16) = n17
& succ(n15) = n16
& succ(n14) = n15
& succ(n13) = n14
& succ(n12) = n13
& succ(n11) = n12
& succ(n10) = n11
& succ(n9) = n10
& succ(n8) = n9
& succ(n7) = n8
& succ(n6) = n7
& succ(n5) = n6
& succ(n4) = n5
& succ(n3) = n4
& succ(n2) = n3
& succ(n1) = n2
&