%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM340+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 08:52:04 AM UTC 2026
% Result : Theorem 13.79s 14.12s
% Output : Proof 13.89s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(rdn0,axiom,
rdn_translate(n0,rdn_pos(rdnn(n0))),
file('NUM005+0.ax',rdn0) ).
fof(rdn1,axiom,
rdn_translate(n1,rdn_pos(rdnn(n1))),
file('NUM005+0.ax',rdn1) ).
fof(rdn2,axiom,
rdn_translate(n2,rdn_pos(rdnn(n2))),
file('NUM005+0.ax',rdn2) ).
fof(rdn3,axiom,
rdn_translate(n3,rdn_pos(rdnn(n3))),
file('NUM005+0.ax',rdn3) ).
fof(rdn4,axiom,
rdn_translate(n4,rdn_pos(rdnn(n4))),
file('NUM005+0.ax',rdn4) ).
fof(rdn5,axiom,
rdn_translate(n5,rdn_pos(rdnn(n5))),
file('NUM005+0.ax',rdn5) ).
fof(rdn6,axiom,
rdn_translate(n6,rdn_pos(rdnn(n6))),
file('NUM005+0.ax',rdn6) ).
fof(rdn7,axiom,
rdn_translate(n7,rdn_pos(rdnn(n7))),
file('NUM005+0.ax',rdn7) ).
fof(rdn8,axiom,
rdn_translate(n8,rdn_pos(rdnn(n8))),
file('NUM005+0.ax',rdn8) ).
fof(rdn9,axiom,
rdn_translate(n9,rdn_pos(rdnn(n9))),
file('NUM005+0.ax',rdn9) ).
fof(rdn10,axiom,
rdn_translate(n10,rdn_pos(rdn(rdnn(n0),rdnn(n1)))),
file('NUM005+0.ax',rdn10) ).
fof(rdn11,axiom,
rdn_translate(n11,rdn_pos(rdn(rdnn(n1),rdnn(n1)))),
file('NUM005+0.ax',rdn11) ).
fof(rdn12,axiom,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
file('NUM005+0.ax',rdn12) ).
fof(rdn13,axiom,
rdn_translate(n13,rdn_pos(rdn(rdnn(n3),rdnn(n1)))),
file('NUM005+0.ax',rdn13) ).
fof(rdn14,axiom,
rdn_translate(n14,rdn_pos(rdn(rdnn(n4),rdnn(n1)))),
file('NUM005+0.ax',rdn14) ).
fof(rdn15,axiom,
rdn_translate(n15,rdn_pos(rdn(rdnn(n5),rdnn(n1)))),
file('NUM005+0.ax',rdn15) ).
fof(rdn16,axiom,
rdn_translate(n16,rdn_pos(rdn(rdnn(n6),rdnn(n1)))),
file('NUM005+0.ax',rdn16) ).
fof(rdn17,axiom,
rdn_translate(n17,rdn_pos(rdn(rdnn(n7),rdnn(n1)))),
file('NUM005+0.ax',rdn17) ).
fof(rdn18,axiom,
rdn_translate(n18,rdn_pos(rdn(rdnn(n8),rdnn(n1)))),
file('NUM005+0.ax',rdn18) ).
fof(rdn19,axiom,
rdn_translate(n19,rdn_pos(rdn(rdnn(n9),rdnn(n1)))),
file('NUM005+0.ax',rdn19) ).
fof(rdn20,axiom,
rdn_translate(n20,rdn_pos(rdn(rdnn(n0),rdnn(n2)))),
file('NUM005+0.ax',rdn20) ).
fof(rdn21,axiom,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
file('NUM005+0.ax',rdn21) ).
fof(rdn22,axiom,
rdn_translate(n22,rdn_pos(rdn(rdnn(n2),rdnn(n2)))),
file('NUM005+0.ax',rdn22) ).
fof(rdn23,axiom,
rdn_translate(n23,rdn_pos(rdn(rdnn(n3),rdnn(n2)))),
file('NUM005+0.ax',rdn23) ).
fof(rdn24,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('NUM005+0.ax',rdn24) ).
fof(rdn25,axiom,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
file('NUM005+0.ax',rdn25) ).
fof(rdn26,axiom,
rdn_translate(n26,rdn_pos(rdn(rdnn(n6),rdnn(n2)))),
file('NUM005+0.ax',rdn26) ).
fof(rdn27,axiom,
rdn_translate(n27,rdn_pos(rdn(rdnn(n7),rdnn(n2)))),
file('NUM005+0.ax',rdn27) ).
fof(rdn28,axiom,
rdn_translate(n28,rdn_pos(rdn(rdnn(n8),rdnn(n2)))),
file('NUM005+0.ax',rdn28) ).
fof(rdn29,axiom,
rdn_translate(n29,rdn_pos(rdn(rdnn(n9),rdnn(n2)))),
file('NUM005+0.ax',rdn29) ).
fof(rdn30,axiom,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
file('NUM005+0.ax',rdn30) ).
fof(rdn31,axiom,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
file('NUM005+0.ax',rdn31) ).
fof(rdn32,axiom,
rdn_translate(n32,rdn_pos(rdn(rdnn(n2),rdnn(n3)))),
file('NUM005+0.ax',rdn32) ).
fof(rdn33,axiom,
rdn_translate(n33,rdn_pos(rdn(rdnn(n3),rdnn(n3)))),
file('NUM005+0.ax',rdn33) ).
fof(rdn34,axiom,
rdn_translate(n34,rdn_pos(rdn(rdnn(n4),rdnn(n3)))),
file('NUM005+0.ax',rdn34) ).
fof(rdn35,axiom,
rdn_translate(n35,rdn_pos(rdn(rdnn(n5),rdnn(n3)))),
file('NUM005+0.ax',rdn35) ).
fof(rdn36,axiom,
rdn_translate(n36,rdn_pos(rdn(rdnn(n6),rdnn(n3)))),
file('NUM005+0.ax',rdn36) ).
fof(rdn37,axiom,
rdn_translate(n37,rdn_pos(rdn(rdnn(n7),rdnn(n3)))),
file('NUM005+0.ax',rdn37) ).
fof(rdn38,axiom,
rdn_translate(n38,rdn_pos(rdn(rdnn(n8),rdnn(n3)))),
file('NUM005+0.ax',rdn38) ).
fof(rdn39,axiom,
rdn_translate(n39,rdn_pos(rdn(rdnn(n9),rdnn(n3)))),
file('NUM005+0.ax',rdn39) ).
fof(rdn40,axiom,
rdn_translate(n40,rdn_pos(rdn(rdnn(n0),rdnn(n4)))),
file('NUM005+0.ax',rdn40) ).
fof(rdn41,axiom,
rdn_translate(n41,rdn_pos(rdn(rdnn(n1),rdnn(n4)))),
file('NUM005+0.ax',rdn41) ).
fof(rdn42,axiom,
rdn_translate(n42,rdn_pos(rdn(rdnn(n2),rdnn(n4)))),
file('NUM005+0.ax',rdn42) ).
fof(rdn43,axiom,
rdn_translate(n43,rdn_pos(rdn(rdnn(n3),rdnn(n4)))),
file('NUM005+0.ax',rdn43) ).
fof(rdn44,axiom,
rdn_translate(n44,rdn_pos(rdn(rdnn(n4),rdnn(n4)))),
file('NUM005+0.ax',rdn44) ).
fof(rdn45,axiom,
rdn_translate(n45,rdn_pos(rdn(rdnn(n5),rdnn(n4)))),
file('NUM005+0.ax',rdn45) ).
fof(rdn46,axiom,
rdn_translate(n46,rdn_pos(rdn(rdnn(n6),rdnn(n4)))),
file('NUM005+0.ax',rdn46) ).
fof(rdn47,axiom,
rdn_translate(n47,rdn_pos(rdn(rdnn(n7),rdnn(n4)))),
file('NUM005+0.ax',rdn47) ).
fof(rdn48,axiom,
rdn_translate(n48,rdn_pos(rdn(rdnn(n8),rdnn(n4)))),
file('NUM005+0.ax',rdn48) ).
fof(rdn49,axiom,
rdn_translate(n49,rdn_pos(rdn(rdnn(n9),rdnn(n4)))),
file('NUM005+0.ax',rdn49) ).
fof(rdn50,axiom,
rdn_translate(n50,rdn_pos(rdn(rdnn(n0),rdnn(n5)))),
file('NUM005+0.ax',rdn50) ).
fof(rdn51,axiom,
rdn_translate(n51,rdn_pos(rdn(rdnn(n1),rdnn(n5)))),
file('NUM005+0.ax',rdn51) ).
fof(rdn52,axiom,
rdn_translate(n52,rdn_pos(rdn(rdnn(n2),rdnn(n5)))),
file('NUM005+0.ax',rdn52) ).
fof(rdn53,axiom,
rdn_translate(n53,rdn_pos(rdn(rdnn(n3),rdnn(n5)))),
file('NUM005+0.ax',rdn53) ).
fof(rdn54,axiom,
rdn_translate(n54,rdn_pos(rdn(rdnn(n4),rdnn(n5)))),
file('NUM005+0.ax',rdn54) ).
fof(rdn55,axiom,
rdn_translate(n55,rdn_pos(rdn(rdnn(n5),rdnn(n5)))),
file('NUM005+0.ax',rdn55) ).
fof(rdn56,axiom,
rdn_translate(n56,rdn_pos(rdn(rdnn(n6),rdnn(n5)))),
file('NUM005+0.ax',rdn56) ).
fof(rdn57,axiom,
rdn_translate(n57,rdn_pos(rdn(rdnn(n7),rdnn(n5)))),
file('NUM005+0.ax',rdn57) ).
fof(rdn58,axiom,
rdn_translate(n58,rdn_pos(rdn(rdnn(n8),rdnn(n5)))),
file('NUM005+0.ax',rdn58) ).
fof(rdn59,axiom,
rdn_translate(n59,rdn_pos(rdn(rdnn(n9),rdnn(n5)))),
file('NUM005+0.ax',rdn59) ).
fof(rdn60,axiom,
rdn_translate(n60,rdn_pos(rdn(rdnn(n0),rdnn(n6)))),
file('NUM005+0.ax',rdn60) ).
fof(rdn61,axiom,
rdn_translate(n61,rdn_pos(rdn(rdnn(n1),rdnn(n6)))),
file('NUM005+0.ax',rdn61) ).
fof(rdn62,axiom,
rdn_translate(n62,rdn_pos(rdn(rdnn(n2),rdnn(n6)))),
file('NUM005+0.ax',rdn62) ).
fof(rdn63,axiom,
rdn_translate(n63,rdn_pos(rdn(rdnn(n3),rdnn(n6)))),
file('NUM005+0.ax',rdn63) ).
fof(rdn64,axiom,
rdn_translate(n64,rdn_pos(rdn(rdnn(n4),rdnn(n6)))),
file('NUM005+0.ax',rdn64) ).
fof(rdn65,axiom,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
file('NUM005+0.ax',rdn65) ).
fof(rdn66,axiom,
rdn_translate(n66,rdn_pos(rdn(rdnn(n6),rdnn(n6)))),
file('NUM005+0.ax',rdn66) ).
fof(rdn67,axiom,
rdn_translate(n67,rdn_pos(rdn(rdnn(n7),rdnn(n6)))),
file('NUM005+0.ax',rdn67) ).
fof(rdn68,axiom,
rdn_translate(n68,rdn_pos(rdn(rdnn(n8),rdnn(n6)))),
file('NUM005+0.ax',rdn68) ).
fof(rdn69,axiom,
rdn_translate(n69,rdn_pos(rdn(rdnn(n9),rdnn(n6)))),
file('NUM005+0.ax',rdn69) ).
fof(rdn70,axiom,
rdn_translate(n70,rdn_pos(rdn(rdnn(n0),rdnn(n7)))),
file('NUM005+0.ax',rdn70) ).
fof(rdn71,axiom,
rdn_translate(n71,rdn_pos(rdn(rdnn(n1),rdnn(n7)))),
file('NUM005+0.ax',rdn71) ).
fof(rdn72,axiom,
rdn_translate(n72,rdn_pos(rdn(rdnn(n2),rdnn(n7)))),
file('NUM005+0.ax',rdn72) ).
fof(rdn73,axiom,
rdn_translate(n73,rdn_pos(rdn(rdnn(n3),rdnn(n7)))),
file('NUM005+0.ax',rdn73) ).
fof(rdn74,axiom,
rdn_translate(n74,rdn_pos(rdn(rdnn(n4),rdnn(n7)))),
file('NUM005+0.ax',rdn74) ).
fof(rdn75,axiom,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
file('NUM005+0.ax',rdn75) ).
fof(rdn76,axiom,
rdn_translate(n76,rdn_pos(rdn(rdnn(n6),rdnn(n7)))),
file('NUM005+0.ax',rdn76) ).
fof(rdn77,axiom,
rdn_translate(n77,rdn_pos(rdn(rdnn(n7),rdnn(n7)))),
file('NUM005+0.ax',rdn77) ).
fof(rdn78,axiom,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
file('NUM005+0.ax',rdn78) ).
fof(rdn79,axiom,
rdn_translate(n79,rdn_pos(rdn(rdnn(n9),rdnn(n7)))),
file('NUM005+0.ax',rdn79) ).
fof(rdn80,axiom,
rdn_translate(n80,rdn_pos(rdn(rdnn(n0),rdnn(n8)))),
file('NUM005+0.ax',rdn80) ).
fof(rdn81,axiom,
rdn_translate(n81,rdn_pos(rdn(rdnn(n1),rdnn(n8)))),
file('NUM005+0.ax',rdn81) ).
fof(rdn82,axiom,
rdn_translate(n82,rdn_pos(rdn(rdnn(n2),rdnn(n8)))),
file('NUM005+0.ax',rdn82) ).
fof(rdn83,axiom,
rdn_translate(n83,rdn_pos(rdn(rdnn(n3),rdnn(n8)))),
file('NUM005+0.ax',rdn83) ).
fof(rdn84,axiom,
rdn_translate(n84,rdn_pos(rdn(rdnn(n4),rdnn(n8)))),
file('NUM005+0.ax',rdn84) ).
fof(rdn85,axiom,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
file('NUM005+0.ax',rdn85) ).
fof(rdn86,axiom,
rdn_translate(n86,rdn_pos(rdn(rdnn(n6),rdnn(n8)))),
file('NUM005+0.ax',rdn86) ).
fof(rdn87,axiom,
rdn_translate(n87,rdn_pos(rdn(rdnn(n7),rdnn(n8)))),
file('NUM005+0.ax',rdn87) ).
fof(rdn88,axiom,
rdn_translate(n88,rdn_pos(rdn(rdnn(n8),rdnn(n8)))),
file('NUM005+0.ax',rdn88) ).
fof(rdn89,axiom,
rdn_translate(n89,rdn_pos(rdn(rdnn(n9),rdnn(n8)))),
file('NUM005+0.ax',rdn89) ).
fof(rdn90,axiom,
rdn_translate(n90,rdn_pos(rdn(rdnn(n0),rdnn(n9)))),
file('NUM005+0.ax',rdn90) ).
fof(rdn91,axiom,
rdn_translate(n91,rdn_pos(rdn(rdnn(n1),rdnn(n9)))),
file('NUM005+0.ax',rdn91) ).
fof(rdn92,axiom,
rdn_translate(n92,rdn_pos(rdn(rdnn(n2),rdnn(n9)))),
file('NUM005+0.ax',rdn92) ).
fof(rdn93,axiom,
rdn_translate(n93,rdn_pos(rdn(rdnn(n3),rdnn(n9)))),
file('NUM005+0.ax',rdn93) ).
fof(rdn94,axiom,
rdn_translate(n94,rdn_pos(rdn(rdnn(n4),rdnn(n9)))),
file('NUM005+0.ax',rdn94) ).
fof(rdn95,axiom,
rdn_translate(n95,rdn_pos(rdn(rdnn(n5),rdnn(n9)))),
file('NUM005+0.ax',rdn95) ).
fof(rdn96,axiom,
rdn_translate(n96,rdn_pos(rdn(rdnn(n6),rdnn(n9)))),
file('NUM005+0.ax',rdn96) ).
fof(rdn97,axiom,
rdn_translate(n97,rdn_pos(rdn(rdnn(n7),rdnn(n9)))),
file('NUM005+0.ax',rdn97) ).
fof(rdn98,axiom,
rdn_translate(n98,rdn_pos(rdn(rdnn(n8),rdnn(n9)))),
file('NUM005+0.ax',rdn98) ).
fof(rdn99,axiom,
rdn_translate(n99,rdn_pos(rdn(rdnn(n9),rdnn(n9)))),
file('NUM005+0.ax',rdn99) ).
fof(rdn100,axiom,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn100) ).
fof(rdn101,axiom,
rdn_translate(n101,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn101) ).
fof(rdn102,axiom,
rdn_translate(n102,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn102) ).
fof(rdn103,axiom,
rdn_translate(n103,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn103) ).
fof(rdn104,axiom,
rdn_translate(n104,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn104) ).
fof(rdn105,axiom,
rdn_translate(n105,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn105) ).
fof(rdn106,axiom,
rdn_translate(n106,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn106) ).
fof(rdn107,axiom,
rdn_translate(n107,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn107) ).
fof(rdn108,axiom,
rdn_translate(n108,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn108) ).
fof(rdn109,axiom,
rdn_translate(n109,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdn109) ).
fof(rdn110,axiom,
rdn_translate(n110,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn110) ).
fof(rdn111,axiom,
rdn_translate(n111,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn111) ).
fof(rdn112,axiom,
rdn_translate(n112,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn112) ).
fof(rdn113,axiom,
rdn_translate(n113,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn113) ).
fof(rdn114,axiom,
rdn_translate(n114,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn114) ).
fof(rdn115,axiom,
rdn_translate(n115,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn115) ).
fof(rdn116,axiom,
rdn_translate(n116,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn116) ).
fof(rdn117,axiom,
rdn_translate(n117,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn117) ).
fof(rdn118,axiom,
rdn_translate(n118,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn118) ).
fof(rdn119,axiom,
rdn_translate(n119,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdn119) ).
fof(rdn120,axiom,
rdn_translate(n120,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn120) ).
fof(rdn121,axiom,
rdn_translate(n121,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn121) ).
fof(rdn122,axiom,
rdn_translate(n122,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn122) ).
fof(rdn123,axiom,
rdn_translate(n123,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn123) ).
fof(rdn124,axiom,
rdn_translate(n124,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn124) ).
fof(rdn125,axiom,
rdn_translate(n125,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn125) ).
fof(rdn126,axiom,
rdn_translate(n126,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn126) ).
fof(rdn127,axiom,
rdn_translate(n127,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdn127) ).
fof(rdnn1,axiom,
rdn_translate(nn1,rdn_neg(rdnn(n1))),
file('NUM005+0.ax',rdnn1) ).
fof(rdnn2,axiom,
rdn_translate(nn2,rdn_neg(rdnn(n2))),
file('NUM005+0.ax',rdnn2) ).
fof(rdnn3,axiom,
rdn_translate(nn3,rdn_neg(rdnn(n3))),
file('NUM005+0.ax',rdnn3) ).
fof(rdnn4,axiom,
rdn_translate(nn4,rdn_neg(rdnn(n4))),
file('NUM005+0.ax',rdnn4) ).
fof(rdnn5,axiom,
rdn_translate(nn5,rdn_neg(rdnn(n5))),
file('NUM005+0.ax',rdnn5) ).
fof(rdnn6,axiom,
rdn_translate(nn6,rdn_neg(rdnn(n6))),
file('NUM005+0.ax',rdnn6) ).
fof(rdnn7,axiom,
rdn_translate(nn7,rdn_neg(rdnn(n7))),
file('NUM005+0.ax',rdnn7) ).
fof(rdnn8,axiom,
rdn_translate(nn8,rdn_neg(rdnn(n8))),
file('NUM005+0.ax',rdnn8) ).
fof(rdnn9,axiom,
rdn_translate(nn9,rdn_neg(rdnn(n9))),
file('NUM005+0.ax',rdnn9) ).
fof(rdnn10,axiom,
rdn_translate(nn10,rdn_neg(rdn(rdnn(n0),rdnn(n1)))),
file('NUM005+0.ax',rdnn10) ).
fof(rdnn11,axiom,
rdn_translate(nn11,rdn_neg(rdn(rdnn(n1),rdnn(n1)))),
file('NUM005+0.ax',rdnn11) ).
fof(rdnn12,axiom,
rdn_translate(nn12,rdn_neg(rdn(rdnn(n2),rdnn(n1)))),
file('NUM005+0.ax',rdnn12) ).
fof(rdnn13,axiom,
rdn_translate(nn13,rdn_neg(rdn(rdnn(n3),rdnn(n1)))),
file('NUM005+0.ax',rdnn13) ).
fof(rdnn14,axiom,
rdn_translate(nn14,rdn_neg(rdn(rdnn(n4),rdnn(n1)))),
file('NUM005+0.ax',rdnn14) ).
fof(rdnn15,axiom,
rdn_translate(nn15,rdn_neg(rdn(rdnn(n5),rdnn(n1)))),
file('NUM005+0.ax',rdnn15) ).
fof(rdnn16,axiom,
rdn_translate(nn16,rdn_neg(rdn(rdnn(n6),rdnn(n1)))),
file('NUM005+0.ax',rdnn16) ).
fof(rdnn17,axiom,
rdn_translate(nn17,rdn_neg(rdn(rdnn(n7),rdnn(n1)))),
file('NUM005+0.ax',rdnn17) ).
fof(rdnn18,axiom,
rdn_translate(nn18,rdn_neg(rdn(rdnn(n8),rdnn(n1)))),
file('NUM005+0.ax',rdnn18) ).
fof(rdnn19,axiom,
rdn_translate(nn19,rdn_neg(rdn(rdnn(n9),rdnn(n1)))),
file('NUM005+0.ax',rdnn19) ).
fof(rdnn20,axiom,
rdn_translate(nn20,rdn_neg(rdn(rdnn(n0),rdnn(n2)))),
file('NUM005+0.ax',rdnn20) ).
fof(rdnn21,axiom,
rdn_translate(nn21,rdn_neg(rdn(rdnn(n1),rdnn(n2)))),
file('NUM005+0.ax',rdnn21) ).
fof(rdnn22,axiom,
rdn_translate(nn22,rdn_neg(rdn(rdnn(n2),rdnn(n2)))),
file('NUM005+0.ax',rdnn22) ).
fof(rdnn23,axiom,
rdn_translate(nn23,rdn_neg(rdn(rdnn(n3),rdnn(n2)))),
file('NUM005+0.ax',rdnn23) ).
fof(rdnn24,axiom,
rdn_translate(nn24,rdn_neg(rdn(rdnn(n4),rdnn(n2)))),
file('NUM005+0.ax',rdnn24) ).
fof(rdnn25,axiom,
rdn_translate(nn25,rdn_neg(rdn(rdnn(n5),rdnn(n2)))),
file('NUM005+0.ax',rdnn25) ).
fof(rdnn26,axiom,
rdn_translate(nn26,rdn_neg(rdn(rdnn(n6),rdnn(n2)))),
file('NUM005+0.ax',rdnn26) ).
fof(rdnn27,axiom,
rdn_translate(nn27,rdn_neg(rdn(rdnn(n7),rdnn(n2)))),
file('NUM005+0.ax',rdnn27) ).
fof(rdnn28,axiom,
rdn_translate(nn28,rdn_neg(rdn(rdnn(n8),rdnn(n2)))),
file('NUM005+0.ax',rdnn28) ).
fof(rdnn29,axiom,
rdn_translate(nn29,rdn_neg(rdn(rdnn(n9),rdnn(n2)))),
file('NUM005+0.ax',rdnn29) ).
fof(rdnn30,axiom,
rdn_translate(nn30,rdn_neg(rdn(rdnn(n0),rdnn(n3)))),
file('NUM005+0.ax',rdnn30) ).
fof(rdnn31,axiom,
rdn_translate(nn31,rdn_neg(rdn(rdnn(n1),rdnn(n3)))),
file('NUM005+0.ax',rdnn31) ).
fof(rdnn32,axiom,
rdn_translate(nn32,rdn_neg(rdn(rdnn(n2),rdnn(n3)))),
file('NUM005+0.ax',rdnn32) ).
fof(rdnn33,axiom,
rdn_translate(nn33,rdn_neg(rdn(rdnn(n3),rdnn(n3)))),
file('NUM005+0.ax',rdnn33) ).
fof(rdnn34,axiom,
rdn_translate(nn34,rdn_neg(rdn(rdnn(n4),rdnn(n3)))),
file('NUM005+0.ax',rdnn34) ).
fof(rdnn35,axiom,
rdn_translate(nn35,rdn_neg(rdn(rdnn(n5),rdnn(n3)))),
file('NUM005+0.ax',rdnn35) ).
fof(rdnn36,axiom,
rdn_translate(nn36,rdn_neg(rdn(rdnn(n6),rdnn(n3)))),
file('NUM005+0.ax',rdnn36) ).
fof(rdnn37,axiom,
rdn_translate(nn37,rdn_neg(rdn(rdnn(n7),rdnn(n3)))),
file('NUM005+0.ax',rdnn37) ).
fof(rdnn38,axiom,
rdn_translate(nn38,rdn_neg(rdn(rdnn(n8),rdnn(n3)))),
file('NUM005+0.ax',rdnn38) ).
fof(rdnn39,axiom,
rdn_translate(nn39,rdn_neg(rdn(rdnn(n9),rdnn(n3)))),
file('NUM005+0.ax',rdnn39) ).
fof(rdnn40,axiom,
rdn_translate(nn40,rdn_neg(rdn(rdnn(n0),rdnn(n4)))),
file('NUM005+0.ax',rdnn40) ).
fof(rdnn41,axiom,
rdn_translate(nn41,rdn_neg(rdn(rdnn(n1),rdnn(n4)))),
file('NUM005+0.ax',rdnn41) ).
fof(rdnn42,axiom,
rdn_translate(nn42,rdn_neg(rdn(rdnn(n2),rdnn(n4)))),
file('NUM005+0.ax',rdnn42) ).
fof(rdnn43,axiom,
rdn_translate(nn43,rdn_neg(rdn(rdnn(n3),rdnn(n4)))),
file('NUM005+0.ax',rdnn43) ).
fof(rdnn44,axiom,
rdn_translate(nn44,rdn_neg(rdn(rdnn(n4),rdnn(n4)))),
file('NUM005+0.ax',rdnn44) ).
fof(rdnn45,axiom,
rdn_translate(nn45,rdn_neg(rdn(rdnn(n5),rdnn(n4)))),
file('NUM005+0.ax',rdnn45) ).
fof(rdnn46,axiom,
rdn_translate(nn46,rdn_neg(rdn(rdnn(n6),rdnn(n4)))),
file('NUM005+0.ax',rdnn46) ).
fof(rdnn47,axiom,
rdn_translate(nn47,rdn_neg(rdn(rdnn(n7),rdnn(n4)))),
file('NUM005+0.ax',rdnn47) ).
fof(rdnn48,axiom,
rdn_translate(nn48,rdn_neg(rdn(rdnn(n8),rdnn(n4)))),
file('NUM005+0.ax',rdnn48) ).
fof(rdnn49,axiom,
rdn_translate(nn49,rdn_neg(rdn(rdnn(n9),rdnn(n4)))),
file('NUM005+0.ax',rdnn49) ).
fof(rdnn50,axiom,
rdn_translate(nn50,rdn_neg(rdn(rdnn(n0),rdnn(n5)))),
file('NUM005+0.ax',rdnn50) ).
fof(rdnn51,axiom,
rdn_translate(nn51,rdn_neg(rdn(rdnn(n1),rdnn(n5)))),
file('NUM005+0.ax',rdnn51) ).
fof(rdnn52,axiom,
rdn_translate(nn52,rdn_neg(rdn(rdnn(n2),rdnn(n5)))),
file('NUM005+0.ax',rdnn52) ).
fof(rdnn53,axiom,
rdn_translate(nn53,rdn_neg(rdn(rdnn(n3),rdnn(n5)))),
file('NUM005+0.ax',rdnn53) ).
fof(rdnn54,axiom,
rdn_translate(nn54,rdn_neg(rdn(rdnn(n4),rdnn(n5)))),
file('NUM005+0.ax',rdnn54) ).
fof(rdnn55,axiom,
rdn_translate(nn55,rdn_neg(rdn(rdnn(n5),rdnn(n5)))),
file('NUM005+0.ax',rdnn55) ).
fof(rdnn56,axiom,
rdn_translate(nn56,rdn_neg(rdn(rdnn(n6),rdnn(n5)))),
file('NUM005+0.ax',rdnn56) ).
fof(rdnn57,axiom,
rdn_translate(nn57,rdn_neg(rdn(rdnn(n7),rdnn(n5)))),
file('NUM005+0.ax',rdnn57) ).
fof(rdnn58,axiom,
rdn_translate(nn58,rdn_neg(rdn(rdnn(n8),rdnn(n5)))),
file('NUM005+0.ax',rdnn58) ).
fof(rdnn59,axiom,
rdn_translate(nn59,rdn_neg(rdn(rdnn(n9),rdnn(n5)))),
file('NUM005+0.ax',rdnn59) ).
fof(rdnn60,axiom,
rdn_translate(nn60,rdn_neg(rdn(rdnn(n0),rdnn(n6)))),
file('NUM005+0.ax',rdnn60) ).
fof(rdnn61,axiom,
rdn_translate(nn61,rdn_neg(rdn(rdnn(n1),rdnn(n6)))),
file('NUM005+0.ax',rdnn61) ).
fof(rdnn62,axiom,
rdn_translate(nn62,rdn_neg(rdn(rdnn(n2),rdnn(n6)))),
file('NUM005+0.ax',rdnn62) ).
fof(rdnn63,axiom,
rdn_translate(nn63,rdn_neg(rdn(rdnn(n3),rdnn(n6)))),
file('NUM005+0.ax',rdnn63) ).
fof(rdnn64,axiom,
rdn_translate(nn64,rdn_neg(rdn(rdnn(n4),rdnn(n6)))),
file('NUM005+0.ax',rdnn64) ).
fof(rdnn65,axiom,
rdn_translate(nn65,rdn_neg(rdn(rdnn(n5),rdnn(n6)))),
file('NUM005+0.ax',rdnn65) ).
fof(rdnn66,axiom,
rdn_translate(nn66,rdn_neg(rdn(rdnn(n6),rdnn(n6)))),
file('NUM005+0.ax',rdnn66) ).
fof(rdnn67,axiom,
rdn_translate(nn67,rdn_neg(rdn(rdnn(n7),rdnn(n6)))),
file('NUM005+0.ax',rdnn67) ).
fof(rdnn68,axiom,
rdn_translate(nn68,rdn_neg(rdn(rdnn(n8),rdnn(n6)))),
file('NUM005+0.ax',rdnn68) ).
fof(rdnn69,axiom,
rdn_translate(nn69,rdn_neg(rdn(rdnn(n9),rdnn(n6)))),
file('NUM005+0.ax',rdnn69) ).
fof(rdnn70,axiom,
rdn_translate(nn70,rdn_neg(rdn(rdnn(n0),rdnn(n7)))),
file('NUM005+0.ax',rdnn70) ).
fof(rdnn71,axiom,
rdn_translate(nn71,rdn_neg(rdn(rdnn(n1),rdnn(n7)))),
file('NUM005+0.ax',rdnn71) ).
fof(rdnn72,axiom,
rdn_translate(nn72,rdn_neg(rdn(rdnn(n2),rdnn(n7)))),
file('NUM005+0.ax',rdnn72) ).
fof(rdnn73,axiom,
rdn_translate(nn73,rdn_neg(rdn(rdnn(n3),rdnn(n7)))),
file('NUM005+0.ax',rdnn73) ).
fof(rdnn74,axiom,
rdn_translate(nn74,rdn_neg(rdn(rdnn(n4),rdnn(n7)))),
file('NUM005+0.ax',rdnn74) ).
fof(rdnn75,axiom,
rdn_translate(nn75,rdn_neg(rdn(rdnn(n5),rdnn(n7)))),
file('NUM005+0.ax',rdnn75) ).
fof(rdnn76,axiom,
rdn_translate(nn76,rdn_neg(rdn(rdnn(n6),rdnn(n7)))),
file('NUM005+0.ax',rdnn76) ).
fof(rdnn77,axiom,
rdn_translate(nn77,rdn_neg(rdn(rdnn(n7),rdnn(n7)))),
file('NUM005+0.ax',rdnn77) ).
fof(rdnn78,axiom,
rdn_translate(nn78,rdn_neg(rdn(rdnn(n8),rdnn(n7)))),
file('NUM005+0.ax',rdnn78) ).
fof(rdnn79,axiom,
rdn_translate(nn79,rdn_neg(rdn(rdnn(n9),rdnn(n7)))),
file('NUM005+0.ax',rdnn79) ).
fof(rdnn80,axiom,
rdn_translate(nn80,rdn_neg(rdn(rdnn(n0),rdnn(n8)))),
file('NUM005+0.ax',rdnn80) ).
fof(rdnn81,axiom,
rdn_translate(nn81,rdn_neg(rdn(rdnn(n1),rdnn(n8)))),
file('NUM005+0.ax',rdnn81) ).
fof(rdnn82,axiom,
rdn_translate(nn82,rdn_neg(rdn(rdnn(n2),rdnn(n8)))),
file('NUM005+0.ax',rdnn82) ).
fof(rdnn83,axiom,
rdn_translate(nn83,rdn_neg(rdn(rdnn(n3),rdnn(n8)))),
file('NUM005+0.ax',rdnn83) ).
fof(rdnn84,axiom,
rdn_translate(nn84,rdn_neg(rdn(rdnn(n4),rdnn(n8)))),
file('NUM005+0.ax',rdnn84) ).
fof(rdnn85,axiom,
rdn_translate(nn85,rdn_neg(rdn(rdnn(n5),rdnn(n8)))),
file('NUM005+0.ax',rdnn85) ).
fof(rdnn86,axiom,
rdn_translate(nn86,rdn_neg(rdn(rdnn(n6),rdnn(n8)))),
file('NUM005+0.ax',rdnn86) ).
fof(rdnn87,axiom,
rdn_translate(nn87,rdn_neg(rdn(rdnn(n7),rdnn(n8)))),
file('NUM005+0.ax',rdnn87) ).
fof(rdnn88,axiom,
rdn_translate(nn88,rdn_neg(rdn(rdnn(n8),rdnn(n8)))),
file('NUM005+0.ax',rdnn88) ).
fof(rdnn89,axiom,
rdn_translate(nn89,rdn_neg(rdn(rdnn(n9),rdnn(n8)))),
file('NUM005+0.ax',rdnn89) ).
fof(rdnn90,axiom,
rdn_translate(nn90,rdn_neg(rdn(rdnn(n0),rdnn(n9)))),
file('NUM005+0.ax',rdnn90) ).
fof(rdnn91,axiom,
rdn_translate(nn91,rdn_neg(rdn(rdnn(n1),rdnn(n9)))),
file('NUM005+0.ax',rdnn91) ).
fof(rdnn92,axiom,
rdn_translate(nn92,rdn_neg(rdn(rdnn(n2),rdnn(n9)))),
file('NUM005+0.ax',rdnn92) ).
fof(rdnn93,axiom,
rdn_translate(nn93,rdn_neg(rdn(rdnn(n3),rdnn(n9)))),
file('NUM005+0.ax',rdnn93) ).
fof(rdnn94,axiom,
rdn_translate(nn94,rdn_neg(rdn(rdnn(n4),rdnn(n9)))),
file('NUM005+0.ax',rdnn94) ).
fof(rdnn95,axiom,
rdn_translate(nn95,rdn_neg(rdn(rdnn(n5),rdnn(n9)))),
file('NUM005+0.ax',rdnn95) ).
fof(rdnn96,axiom,
rdn_translate(nn96,rdn_neg(rdn(rdnn(n6),rdnn(n9)))),
file('NUM005+0.ax',rdnn96) ).
fof(rdnn97,axiom,
rdn_translate(nn97,rdn_neg(rdn(rdnn(n7),rdnn(n9)))),
file('NUM005+0.ax',rdnn97) ).
fof(rdnn98,axiom,
rdn_translate(nn98,rdn_neg(rdn(rdnn(n8),rdnn(n9)))),
file('NUM005+0.ax',rdnn98) ).
fof(rdnn99,axiom,
rdn_translate(nn99,rdn_neg(rdn(rdnn(n9),rdnn(n9)))),
file('NUM005+0.ax',rdnn99) ).
fof(rdnn100,axiom,
rdn_translate(nn100,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn100) ).
fof(rdnn101,axiom,
rdn_translate(nn101,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn101) ).
fof(rdnn102,axiom,
rdn_translate(nn102,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn102) ).
fof(rdnn103,axiom,
rdn_translate(nn103,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn103) ).
fof(rdnn104,axiom,
rdn_translate(nn104,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn104) ).
fof(rdnn105,axiom,
rdn_translate(nn105,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn105) ).
fof(rdnn106,axiom,
rdn_translate(nn106,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn106) ).
fof(rdnn107,axiom,
rdn_translate(nn107,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn107) ).
fof(rdnn108,axiom,
rdn_translate(nn108,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn108) ).
fof(rdnn109,axiom,
rdn_translate(nn109,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
file('NUM005+0.ax',rdnn109) ).
fof(rdnn110,axiom,
rdn_translate(nn110,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn110) ).
fof(rdnn111,axiom,
rdn_translate(nn111,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn111) ).
fof(rdnn112,axiom,
rdn_translate(nn112,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn112) ).
fof(rdnn113,axiom,
rdn_translate(nn113,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn113) ).
fof(rdnn114,axiom,
rdn_translate(nn114,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn114) ).
fof(rdnn115,axiom,
rdn_translate(nn115,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn115) ).
fof(rdnn116,axiom,
rdn_translate(nn116,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn116) ).
fof(rdnn117,axiom,
rdn_translate(nn117,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn117) ).
fof(rdnn118,axiom,
rdn_translate(nn118,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn118) ).
fof(rdnn119,axiom,
rdn_translate(nn119,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
file('NUM005+0.ax',rdnn119) ).
fof(rdnn120,axiom,
rdn_translate(nn120,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn120) ).
fof(rdnn121,axiom,
rdn_translate(nn121,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn121) ).
fof(rdnn122,axiom,
rdn_translate(nn122,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn122) ).
fof(rdnn123,axiom,
rdn_translate(nn123,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn123) ).
fof(rdnn124,axiom,
rdn_translate(nn124,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn124) ).
fof(rdnn125,axiom,
rdn_translate(nn125,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn125) ).
fof(rdnn126,axiom,
rdn_translate(nn126,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn126) ).
fof(rdnn127,axiom,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn127) ).
fof(rdnn128,axiom,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
file('NUM005+0.ax',rdnn128) ).
fof(rdn_digit1,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('NUM005+1.ax',rdn_digit1) ).
fof(rdn_digit2,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('NUM005+1.ax',rdn_digit2) ).
fof(rdn_digit3,axiom,
rdn_non_zero_digit(rdnn(n3)),
file('NUM005+1.ax',rdn_digit3) ).
fof(rdn_digit4,axiom,
rdn_non_zero_digit(rdnn(n4)),
file('NUM005+1.ax',rdn_digit4) ).
fof(rdn_digit5,axiom,
rdn_non_zero_digit(rdnn(n5)),
file('NUM005+1.ax',rdn_digit5) ).
fof(rdn_digit6,axiom,
rdn_non_zero_digit(rdnn(n6)),
file('NUM005+1.ax',rdn_digit6) ).
fof(rdn_digit7,axiom,
rdn_non_zero_digit(rdnn(n7)),
file('NUM005+1.ax',rdn_digit7) ).
fof(rdn_digit8,axiom,
rdn_non_zero_digit(rdnn(n8)),
file('NUM005+1.ax',rdn_digit8) ).
fof(rdn_digit9,axiom,
rdn_non_zero_digit(rdnn(n9)),
file('NUM005+1.ax',rdn_digit9) ).
fof(rdn_positive_less01,axiom,
rdn_positive_less(rdnn(n0),rdnn(n1)),
file('NUM005+1.ax',rdn_positive_less01) ).
fof(rdn_positive_less12,axiom,
rdn_positive_less(rdnn(n1),rdnn(n2)),
file('NUM005+1.ax',rdn_positive_less12) ).
fof(rdn_positive_less23,axiom,
rdn_positive_less(rdnn(n2),rdnn(n3)),
file('NUM005+1.ax',rdn_positive_less23) ).
fof(rdn_positive_less34,axiom,
rdn_positive_less(rdnn(n3),rdnn(n4)),
file('NUM005+1.ax',rdn_positive_less34) ).
fof(rdn_positive_less45,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('NUM005+1.ax',rdn_positive_less45) ).
fof(rdn_positive_less56,axiom,
rdn_positive_less(rdnn(n5),rdnn(n6)),
file('NUM005+1.ax',rdn_positive_less56) ).
fof(rdn_positive_less67,axiom,
rdn_positive_less(rdnn(n6),rdnn(n7)),
file('NUM005+1.ax',rdn_positive_less67) ).
fof(rdn_positive_less78,axiom,
rdn_positive_less(rdnn(n7),rdnn(n8)),
file('NUM005+1.ax',rdn_positive_less78) ).
fof(rdn_positive_less89,axiom,
rdn_positive_less(rdnn(n8),rdnn(n9)),
file('NUM005+1.ax',rdn_positive_less89) ).
fof(rdn_positive_less_transitivity,axiom,
! [X,Y,Z] :
( ( rdn_positive_less(rdnn(Y),rdnn(Z))
& rdn_positive_less(rdnn(X),rdnn(Y)) )
=> rdn_positive_less(rdnn(X),rdnn(Z)) ),
file('NUM005+1.ax',rdn_positive_less_transitivity) ).
fof(rdn_positive_less_multi_digit_high,axiom,
! [Ds,Os,Db,Ob] :
( rdn_positive_less(Os,Ob)
=> rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob)) ),
file('NUM005+1.ax',rdn_positive_less_multi_digit_high) ).
fof(rdn_positive_less_multi_digit_low,axiom,
! [Ds,O,Db] :
( ( rdn_non_zero(O)
& rdn_positive_less(rdnn(Ds),rdnn(Db)) )
=> rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ),
file('NUM005+1.ax',rdn_positive_less_multi_digit_low) ).
fof(rdn_extra_digits_positive_less,axiom,
! [D,Db,Ob] :
( rdn_non_zero(Ob)
=> rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob)) ),
file('NUM005+1.ax',rdn_extra_digits_positive_less) ).
fof(rdn_non_zero_by_digit,axiom,
! [X] :
( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) ),
file('NUM005+1.ax',rdn_non_zero_by_digit) ).
fof(rdn_non_zero_by_structure,axiom,
! [D,O] :
( rdn_non_zero(O)
=> rdn_non_zero(rdn(rdnn(D),O)) ),
file('NUM005+1.ax',rdn_non_zero_by_structure) ).
fof(less_entry_point_pos_pos,axiom,
! [X,Y,RDN_X,RDN_Y] :
( ( rdn_positive_less(RDN_X,RDN_Y)
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> less(X,Y) ),
file('NUM005+1.ax',less_entry_point_pos_pos) ).
fof(less_entry_point_neg_pos,axiom,
! [X,Y,RDN_X,RDN_Y] :
( ( rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_neg(RDN_X)) )
=> less(X,Y) ),
file('NUM005+1.ax',less_entry_point_neg_pos) ).
fof(less_entry_point_neg_neg,axiom,
! [X,Y,RDN_X,RDN_Y] :
( ( rdn_positive_less(RDN_Y,RDN_X)
& rdn_translate(Y,rdn_neg(RDN_Y))
& rdn_translate(X,rdn_neg(RDN_X)) )
=> less(X,Y) ),
file('NUM005+1.ax',less_entry_point_neg_neg) ).
fof(less_property,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('NUM005+1.ax',less_property) ).
fof(less_or_equal,axiom,
! [X,Y] :
( less_or_equal(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('NUM005+1.ax',less_or_equal) ).
fof(less_successor,axiom,
! [X,Y,Z] :
( ( less(Z,Y)
& sum(X,n1,Y) )
=> less_or_equal(Z,X) ),
file('NUM005+1.ax',less_successor) ).
fof(sum_entry_point_pos_pos,axiom,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( ( rdn_translate(Z,rdn_pos(RDN_Z))
& rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Y,RDN_Z)
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> sum(X,Y,Z) ),
file('NUM005+2.ax',sum_entry_point_pos_pos) ).
fof(sum_entry_point_neg_neg,axiom,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( ( rdn_translate(Z,rdn_neg(RDN_Z))
& rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Y,RDN_Z)
& rdn_translate(Y,rdn_neg(RDN_Y))
& rdn_translate(X,rdn_neg(RDN_X)) )
=> sum(X,Y,Z) ),
file('NUM005+2.ax',sum_entry_point_neg_neg) ).
fof(sum_entry_point_pos_neg_1,axiom,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( ( rdn_translate(Z,rdn_neg(RDN_Z))
& rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Z,RDN_Y)
& rdn_positive_less(RDN_X,RDN_Y)
& rdn_translate(Y,rdn_neg(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> sum(X,Y,Z) ),
file('NUM005+2.ax',sum_entry_point_pos_neg_1) ).
fof(sum_entry_point_pos_neg_2,axiom,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( ( rdn_translate(Z,rdn_pos(RDN_Z))
& rdn_add_with_carry(rdnn(n0),RDN_Y,RDN_Z,RDN_X)
& rdn_positive_less(RDN_Y,RDN_X)
& rdn_translate(Y,rdn_neg(RDN_Y))
& rdn_translate(X,rdn_pos(RDN_X)) )
=> sum(X,Y,Z) ),
file('NUM005+2.ax',sum_entry_point_pos_neg_2) ).
fof(sum_entry_point_posx_negx,axiom,
! [POS_X,NEG_X,RDN_X] :
( ( rdn_translate(NEG_X,rdn_neg(RDN_X))
& rdn_translate(POS_X,rdn_pos(RDN_X)) )
=> sum(POS_X,NEG_X,n0) ),
file('NUM005+2.ax',sum_entry_point_posx_negx) ).
fof(sum_entry_point_neg_pos,axiom,
! [X,Y,Z,RDN_X,RDN_Y] :
( ( sum(Y,X,Z)
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_translate(X,rdn_neg(RDN_X)) )
=> sum(X,Y,Z) ),
file('NUM005+2.ax',sum_entry_point_neg_pos) ).
fof(unique_sum,axiom,
! [X,Y,Z1,Z2] :
( ( sum(X,Y,Z2)
& sum(X,Y,Z1) )
=> Z1 = Z2 ),
file('NUM005+2.ax',unique_sum) ).
fof(unique_LHS,axiom,
! [X1,X2,Y,Z] :
( ( sum(X2,Y,Z)
& sum(X1,Y,Z) )
=> X1 = X2 ),
file('NUM005+2.ax',unique_LHS) ).
fof(unique_RHS,axiom,
! [X,Y1,Y2,Z] :
( ( sum(X,Y2,Z)
& sum(X,Y1,Z) )
=> Y1 = Y2 ),
file('NUM005+2.ax',unique_RHS) ).
fof(minus_entry_point,axiom,
! [X,Y,Z] :
( sum(Y,Z,X)
<=> difference(X,Y,Z) ),
file('NUM005+2.ax',minus_entry_point) ).
fof(add_digit_digit_digit,axiom,
! [C,D1,D2,RD,ID] :
( ( rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(n0))
& rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(n0)) )
=> rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdnn(RD)) ),
file('NUM005+2.ax',add_digit_digit_digit) ).
fof(add_digit_digit_rdn,axiom,
! [C,D1,D2,ID,RD,IC1,IC2] :
( ( rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(n1),rdnn(n0))
& rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
& rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) )
=> rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdn(rdnn(RD),rdnn(n1))) ),
file('NUM005+2.ax',add_digit_digit_rdn) ).
fof(add_digit_rdn_rdn,axiom,
! [C,D1,D2,O2,RD,RO,ID,IC1,IC2,NC] :
( ( rdn_non_zero(RO)
& rdn_non_zero(O2)
& rdn_add_with_carry(rdnn(NC),rdnn(n0),O2,RO)
& rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(NC),rdnn(n0))
& rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
& rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) )
=> rdn_add_with_carry(rdnn(C),rdnn(D1),rdn(rdnn(D2),O2),rdn(rdnn(RD),RO)) ),
file('NUM005+2.ax',add_digit_rdn_rdn) ).
fof(add_rdn_rdn_rdn,axiom,
! [C,D1,O1,D2,O2,RD,RO,ID,IC1,IC2,RC] :
( ( rdn_non_zero(RO)
& rdn_non_zero(O2)
& rdn_non_zero(O1)
& rdn_add_with_carry(rdnn(RC),O1,O2,RO)
& rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(RC),rdnn(n0))
& rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
& rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) )
=> rdn_add_with_carry(rdnn(C),rdn(rdnn(D1),O1),rdn(rdnn(D2),O2),rdn(rdnn(RD),RO)) ),
file('NUM005+2.ax',add_rdn_rdn_rdn) ).
fof(add_rdn_digit_rdn,axiom,
! [C,D1,O1,D2,RD,RO] :
( rdn_add_with_carry(rdnn(C),rdnn(D2),rdn(rdnn(D1),O1),rdn(rdnn(RD),RO))
=> rdn_add_with_carry(rdnn(C),rdn(rdnn(D1),O1),rdnn(D2),rdn(rdnn(RD),RO)) ),
file('NUM005+2.ax',add_rdn_digit_rdn) ).
fof(rdn_digit_add_n0_n0_n0_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n0_n0_n0) ).
fof(rdn_digit_add_n0_n1_n1_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(n1),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n1_n1_n0) ).
fof(rdn_digit_add_n0_n2_n2_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(n2),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n2_n2_n0) ).
fof(rdn_digit_add_n0_n3_n3_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n3),rdnn(n3),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n3_n3_n0) ).
fof(rdn_digit_add_n0_n4_n4_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n4),rdnn(n4),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n4_n4_n0) ).
fof(rdn_digit_add_n0_n5_n5_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n5),rdnn(n5),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n5_n5_n0) ).
fof(rdn_digit_add_n0_n6_n6_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n6),rdnn(n6),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n6_n6_n0) ).
fof(rdn_digit_add_n0_n7_n7_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n7),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n7_n7_n0) ).
fof(rdn_digit_add_n0_n8_n8_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n8),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n8_n8_n0) ).
fof(rdn_digit_add_n0_n9_n9_n0,axiom,
rdn_digit_add(rdnn(n0),rdnn(n9),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n0_n9_n9_n0) ).
fof(rdn_digit_add_n1_n0_n1_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n0_n1_n0) ).
fof(rdn_digit_add_n1_n1_n2_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n1),rdnn(n2),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n1_n2_n0) ).
fof(rdn_digit_add_n1_n2_n3_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n2),rdnn(n3),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n2_n3_n0) ).
fof(rdn_digit_add_n1_n3_n4_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n3),rdnn(n4),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n3_n4_n0) ).
fof(rdn_digit_add_n1_n4_n5_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n4),rdnn(n5),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n4_n5_n0) ).
fof(rdn_digit_add_n1_n5_n6_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n5),rdnn(n6),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n5_n6_n0) ).
fof(rdn_digit_add_n1_n6_n7_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n6),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n6_n7_n0) ).
fof(rdn_digit_add_n1_n7_n8_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n7_n8_n0) ).
fof(rdn_digit_add_n1_n8_n9_n0,axiom,
rdn_digit_add(rdnn(n1),rdnn(n8),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n1_n8_n9_n0) ).
fof(rdn_digit_add_n1_n9_n0_n1,axiom,
rdn_digit_add(rdnn(n1),rdnn(n9),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n1_n9_n0_n1) ).
fof(rdn_digit_add_n2_n0_n2_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n0_n2_n0) ).
fof(rdn_digit_add_n2_n1_n3_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n1),rdnn(n3),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n1_n3_n0) ).
fof(rdn_digit_add_n2_n2_n4_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n2),rdnn(n4),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n2_n4_n0) ).
fof(rdn_digit_add_n2_n3_n5_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n3),rdnn(n5),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n3_n5_n0) ).
fof(rdn_digit_add_n2_n4_n6_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n4),rdnn(n6),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n4_n6_n0) ).
fof(rdn_digit_add_n2_n5_n7_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n5),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n5_n7_n0) ).
fof(rdn_digit_add_n2_n6_n8_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n6),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n6_n8_n0) ).
fof(rdn_digit_add_n2_n7_n9_n0,axiom,
rdn_digit_add(rdnn(n2),rdnn(n7),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n2_n7_n9_n0) ).
fof(rdn_digit_add_n2_n8_n0_n1,axiom,
rdn_digit_add(rdnn(n2),rdnn(n8),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n2_n8_n0_n1) ).
fof(rdn_digit_add_n2_n9_n1_n1,axiom,
rdn_digit_add(rdnn(n2),rdnn(n9),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n2_n9_n1_n1) ).
fof(rdn_digit_add_n3_n0_n3_n0,axiom,
rdn_digit_add(rdnn(n3),rdnn(n0),rdnn(n3),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n3_n0_n3_n0) ).
fof(rdn_digit_add_n3_n1_n4_n0,axiom,
rdn_digit_add(rdnn(n3),rdnn(n1),rdnn(n4),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n3_n1_n4_n0) ).
fof(rdn_digit_add_n3_n2_n5_n0,axiom,
rdn_digit_add(rdnn(n3),rdnn(n2),rdnn(n5),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n3_n2_n5_n0) ).
fof(rdn_digit_add_n3_n3_n6_n0,axiom,
rdn_digit_add(rdnn(n3),rdnn(n3),rdnn(n6),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n3_n3_n6_n0) ).
fof(rdn_digit_add_n3_n4_n7_n0,axiom,
rdn_digit_add(rdnn(n3),rdnn(n4),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n3_n4_n7_n0) ).
fof(rdn_digit_add_n3_n5_n8_n0,axiom,
rdn_digit_add(rdnn(n3),rdnn(n5),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n3_n5_n8_n0) ).
fof(rdn_digit_add_n3_n6_n9_n0,axiom,
rdn_digit_add(rdnn(n3),rdnn(n6),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n3_n6_n9_n0) ).
fof(rdn_digit_add_n3_n7_n0_n1,axiom,
rdn_digit_add(rdnn(n3),rdnn(n7),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n3_n7_n0_n1) ).
fof(rdn_digit_add_n3_n8_n1_n1,axiom,
rdn_digit_add(rdnn(n3),rdnn(n8),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n3_n8_n1_n1) ).
fof(rdn_digit_add_n3_n9_n2_n1,axiom,
rdn_digit_add(rdnn(n3),rdnn(n9),rdnn(n2),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n3_n9_n2_n1) ).
fof(rdn_digit_add_n4_n0_n4_n0,axiom,
rdn_digit_add(rdnn(n4),rdnn(n0),rdnn(n4),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n4_n0_n4_n0) ).
fof(rdn_digit_add_n4_n1_n5_n0,axiom,
rdn_digit_add(rdnn(n4),rdnn(n1),rdnn(n5),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n4_n1_n5_n0) ).
fof(rdn_digit_add_n4_n2_n6_n0,axiom,
rdn_digit_add(rdnn(n4),rdnn(n2),rdnn(n6),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n4_n2_n6_n0) ).
fof(rdn_digit_add_n4_n3_n7_n0,axiom,
rdn_digit_add(rdnn(n4),rdnn(n3),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n4_n3_n7_n0) ).
fof(rdn_digit_add_n4_n4_n8_n0,axiom,
rdn_digit_add(rdnn(n4),rdnn(n4),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n4_n4_n8_n0) ).
fof(rdn_digit_add_n4_n5_n9_n0,axiom,
rdn_digit_add(rdnn(n4),rdnn(n5),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n4_n5_n9_n0) ).
fof(rdn_digit_add_n4_n6_n0_n1,axiom,
rdn_digit_add(rdnn(n4),rdnn(n6),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n4_n6_n0_n1) ).
fof(rdn_digit_add_n4_n7_n1_n1,axiom,
rdn_digit_add(rdnn(n4),rdnn(n7),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n4_n7_n1_n1) ).
fof(rdn_digit_add_n4_n8_n2_n1,axiom,
rdn_digit_add(rdnn(n4),rdnn(n8),rdnn(n2),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n4_n8_n2_n1) ).
fof(rdn_digit_add_n4_n9_n3_n1,axiom,
rdn_digit_add(rdnn(n4),rdnn(n9),rdnn(n3),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n4_n9_n3_n1) ).
fof(rdn_digit_add_n5_n0_n5_n0,axiom,
rdn_digit_add(rdnn(n5),rdnn(n0),rdnn(n5),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n5_n0_n5_n0) ).
fof(rdn_digit_add_n5_n1_n6_n0,axiom,
rdn_digit_add(rdnn(n5),rdnn(n1),rdnn(n6),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n5_n1_n6_n0) ).
fof(rdn_digit_add_n5_n2_n7_n0,axiom,
rdn_digit_add(rdnn(n5),rdnn(n2),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n5_n2_n7_n0) ).
fof(rdn_digit_add_n5_n3_n8_n0,axiom,
rdn_digit_add(rdnn(n5),rdnn(n3),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n5_n3_n8_n0) ).
fof(rdn_digit_add_n5_n4_n9_n0,axiom,
rdn_digit_add(rdnn(n5),rdnn(n4),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n5_n4_n9_n0) ).
fof(rdn_digit_add_n5_n5_n0_n1,axiom,
rdn_digit_add(rdnn(n5),rdnn(n5),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n5_n5_n0_n1) ).
fof(rdn_digit_add_n5_n6_n1_n1,axiom,
rdn_digit_add(rdnn(n5),rdnn(n6),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n5_n6_n1_n1) ).
fof(rdn_digit_add_n5_n7_n2_n1,axiom,
rdn_digit_add(rdnn(n5),rdnn(n7),rdnn(n2),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n5_n7_n2_n1) ).
fof(rdn_digit_add_n5_n8_n3_n1,axiom,
rdn_digit_add(rdnn(n5),rdnn(n8),rdnn(n3),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n5_n8_n3_n1) ).
fof(rdn_digit_add_n5_n9_n4_n1,axiom,
rdn_digit_add(rdnn(n5),rdnn(n9),rdnn(n4),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n5_n9_n4_n1) ).
fof(rdn_digit_add_n6_n0_n6_n0,axiom,
rdn_digit_add(rdnn(n6),rdnn(n0),rdnn(n6),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n6_n0_n6_n0) ).
fof(rdn_digit_add_n6_n1_n7_n0,axiom,
rdn_digit_add(rdnn(n6),rdnn(n1),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n6_n1_n7_n0) ).
fof(rdn_digit_add_n6_n2_n8_n0,axiom,
rdn_digit_add(rdnn(n6),rdnn(n2),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n6_n2_n8_n0) ).
fof(rdn_digit_add_n6_n3_n9_n0,axiom,
rdn_digit_add(rdnn(n6),rdnn(n3),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n6_n3_n9_n0) ).
fof(rdn_digit_add_n6_n4_n0_n1,axiom,
rdn_digit_add(rdnn(n6),rdnn(n4),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n6_n4_n0_n1) ).
fof(rdn_digit_add_n6_n5_n1_n1,axiom,
rdn_digit_add(rdnn(n6),rdnn(n5),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n6_n5_n1_n1) ).
fof(rdn_digit_add_n6_n6_n2_n1,axiom,
rdn_digit_add(rdnn(n6),rdnn(n6),rdnn(n2),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n6_n6_n2_n1) ).
fof(rdn_digit_add_n6_n7_n3_n1,axiom,
rdn_digit_add(rdnn(n6),rdnn(n7),rdnn(n3),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n6_n7_n3_n1) ).
fof(rdn_digit_add_n6_n8_n4_n1,axiom,
rdn_digit_add(rdnn(n6),rdnn(n8),rdnn(n4),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n6_n8_n4_n1) ).
fof(rdn_digit_add_n6_n9_n5_n1,axiom,
rdn_digit_add(rdnn(n6),rdnn(n9),rdnn(n5),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n6_n9_n5_n1) ).
fof(rdn_digit_add_n7_n0_n7_n0,axiom,
rdn_digit_add(rdnn(n7),rdnn(n0),rdnn(n7),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n7_n0_n7_n0) ).
fof(rdn_digit_add_n7_n1_n8_n0,axiom,
rdn_digit_add(rdnn(n7),rdnn(n1),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n7_n1_n8_n0) ).
fof(rdn_digit_add_n7_n2_n9_n0,axiom,
rdn_digit_add(rdnn(n7),rdnn(n2),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n7_n2_n9_n0) ).
fof(rdn_digit_add_n7_n3_n0_n1,axiom,
rdn_digit_add(rdnn(n7),rdnn(n3),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n7_n3_n0_n1) ).
fof(rdn_digit_add_n7_n4_n1_n1,axiom,
rdn_digit_add(rdnn(n7),rdnn(n4),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n7_n4_n1_n1) ).
fof(rdn_digit_add_n7_n5_n2_n1,axiom,
rdn_digit_add(rdnn(n7),rdnn(n5),rdnn(n2),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n7_n5_n2_n1) ).
fof(rdn_digit_add_n7_n6_n3_n1,axiom,
rdn_digit_add(rdnn(n7),rdnn(n6),rdnn(n3),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n7_n6_n3_n1) ).
fof(rdn_digit_add_n7_n7_n4_n1,axiom,
rdn_digit_add(rdnn(n7),rdnn(n7),rdnn(n4),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n7_n7_n4_n1) ).
fof(rdn_digit_add_n7_n8_n5_n1,axiom,
rdn_digit_add(rdnn(n7),rdnn(n8),rdnn(n5),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n7_n8_n5_n1) ).
fof(rdn_digit_add_n7_n9_n6_n1,axiom,
rdn_digit_add(rdnn(n7),rdnn(n9),rdnn(n6),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n7_n9_n6_n1) ).
fof(rdn_digit_add_n8_n0_n8_n0,axiom,
rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(n8),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n8_n0_n8_n0) ).
fof(rdn_digit_add_n8_n1_n9_n0,axiom,
rdn_digit_add(rdnn(n8),rdnn(n1),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n8_n1_n9_n0) ).
fof(rdn_digit_add_n8_n2_n0_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n2),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n2_n0_n1) ).
fof(rdn_digit_add_n8_n3_n1_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n3),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n3_n1_n1) ).
fof(rdn_digit_add_n8_n4_n2_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n4),rdnn(n2),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n4_n2_n1) ).
fof(rdn_digit_add_n8_n5_n3_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n5),rdnn(n3),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n5_n3_n1) ).
fof(rdn_digit_add_n8_n6_n4_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n6),rdnn(n4),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n6_n4_n1) ).
fof(rdn_digit_add_n8_n7_n5_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n7),rdnn(n5),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n7_n5_n1) ).
fof(rdn_digit_add_n8_n8_n6_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n8),rdnn(n6),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n8_n6_n1) ).
fof(rdn_digit_add_n8_n9_n7_n1,axiom,
rdn_digit_add(rdnn(n8),rdnn(n9),rdnn(n7),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n8_n9_n7_n1) ).
fof(rdn_digit_add_n9_n0_n9_n0,axiom,
rdn_digit_add(rdnn(n9),rdnn(n0),rdnn(n9),rdnn(n0)),
file('NUM005+2.ax',rdn_digit_add_n9_n0_n9_n0) ).
fof(rdn_digit_add_n9_n1_n0_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n1),rdnn(n0),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n1_n0_n1) ).
fof(rdn_digit_add_n9_n2_n1_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n2),rdnn(n1),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n2_n1_n1) ).
fof(rdn_digit_add_n9_n3_n2_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n3),rdnn(n2),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n3_n2_n1) ).
fof(rdn_digit_add_n9_n4_n3_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n4),rdnn(n3),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n4_n3_n1) ).
fof(rdn_digit_add_n9_n5_n4_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n5),rdnn(n4),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n5_n4_n1) ).
fof(rdn_digit_add_n9_n6_n5_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n6),rdnn(n5),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n6_n5_n1) ).
fof(rdn_digit_add_n9_n7_n6_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n7),rdnn(n6),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n7_n6_n1) ).
fof(rdn_digit_add_n9_n8_n7_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n8),rdnn(n7),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n8_n7_n1) ).
fof(rdn_digit_add_n9_n9_n8_n1,axiom,
rdn_digit_add(rdnn(n9),rdnn(n9),rdnn(n8),rdnn(n1)),
file('NUM005+2.ax',rdn_digit_add_n9_n9_n8_n1) ).
fof(diff_zero_identity,conjecture,
? [X] : difference(X,n0,X),
file('theBenchmark.p',diff_zero_identity) ).
fof(f_1_1,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(fof_nnf,[status(thm)],[rdn0]) ).
cnf(f_1_2,plain,
rdn_translate(n0,rdn_pos(rdnn(n0))),
inference(clausify,[status(thm)],[f_1_1]) ).
fof(f_2_1,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(fof_nnf,[status(thm)],[rdn1]) ).
cnf(f_2_2,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(clausify,[status(thm)],[f_2_1]) ).
fof(f_3_1,plain,
rdn_translate(n2,rdn_pos(rdnn(n2))),
inference(fof_nnf,[status(thm)],[rdn2]) ).
cnf(f_3_2,plain,
rdn_translate(n2,rdn_pos(rdnn(n2))),
inference(clausify,[status(thm)],[f_3_1]) ).
fof(f_4_1,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(fof_nnf,[status(thm)],[rdn3]) ).
cnf(f_4_2,plain,
rdn_translate(n3,rdn_pos(rdnn(n3))),
inference(clausify,[status(thm)],[f_4_1]) ).
fof(f_5_1,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(fof_nnf,[status(thm)],[rdn4]) ).
cnf(f_5_2,plain,
rdn_translate(n4,rdn_pos(rdnn(n4))),
inference(clausify,[status(thm)],[f_5_1]) ).
fof(f_6_1,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(fof_nnf,[status(thm)],[rdn5]) ).
cnf(f_6_2,plain,
rdn_translate(n5,rdn_pos(rdnn(n5))),
inference(clausify,[status(thm)],[f_6_1]) ).
fof(f_7_1,plain,
rdn_translate(n6,rdn_pos(rdnn(n6))),
inference(fof_nnf,[status(thm)],[rdn6]) ).
cnf(f_7_2,plain,
rdn_translate(n6,rdn_pos(rdnn(n6))),
inference(clausify,[status(thm)],[f_7_1]) ).
fof(f_8_1,plain,
rdn_translate(n7,rdn_pos(rdnn(n7))),
inference(fof_nnf,[status(thm)],[rdn7]) ).
cnf(f_8_2,plain,
rdn_translate(n7,rdn_pos(rdnn(n7))),
inference(clausify,[status(thm)],[f_8_1]) ).
fof(f_9_1,plain,
rdn_translate(n8,rdn_pos(rdnn(n8))),
inference(fof_nnf,[status(thm)],[rdn8]) ).
cnf(f_9_2,plain,
rdn_translate(n8,rdn_pos(rdnn(n8))),
inference(clausify,[status(thm)],[f_9_1]) ).
fof(f_10_1,plain,
rdn_translate(n9,rdn_pos(rdnn(n9))),
inference(fof_nnf,[status(thm)],[rdn9]) ).
cnf(f_10_2,plain,
rdn_translate(n9,rdn_pos(rdnn(n9))),
inference(clausify,[status(thm)],[f_10_1]) ).
fof(f_11_1,plain,
rdn_translate(n10,rdn_pos(rdn(rdnn(n0),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn10]) ).
cnf(f_11_2,plain,
rdn_translate(n10,rdn_pos(rdn(rdnn(n0),rdnn(n1)))),
inference(clausify,[status(thm)],[f_11_1]) ).
fof(f_12_1,plain,
rdn_translate(n11,rdn_pos(rdn(rdnn(n1),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn11]) ).
cnf(f_12_2,plain,
rdn_translate(n11,rdn_pos(rdn(rdnn(n1),rdnn(n1)))),
inference(clausify,[status(thm)],[f_12_1]) ).
fof(f_13_1,plain,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn12]) ).
cnf(f_13_2,plain,
rdn_translate(n12,rdn_pos(rdn(rdnn(n2),rdnn(n1)))),
inference(clausify,[status(thm)],[f_13_1]) ).
fof(f_14_1,plain,
rdn_translate(n13,rdn_pos(rdn(rdnn(n3),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn13]) ).
cnf(f_14_2,plain,
rdn_translate(n13,rdn_pos(rdn(rdnn(n3),rdnn(n1)))),
inference(clausify,[status(thm)],[f_14_1]) ).
fof(f_15_1,plain,
rdn_translate(n14,rdn_pos(rdn(rdnn(n4),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn14]) ).
cnf(f_15_2,plain,
rdn_translate(n14,rdn_pos(rdn(rdnn(n4),rdnn(n1)))),
inference(clausify,[status(thm)],[f_15_1]) ).
fof(f_16_1,plain,
rdn_translate(n15,rdn_pos(rdn(rdnn(n5),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn15]) ).
cnf(f_16_2,plain,
rdn_translate(n15,rdn_pos(rdn(rdnn(n5),rdnn(n1)))),
inference(clausify,[status(thm)],[f_16_1]) ).
fof(f_17_1,plain,
rdn_translate(n16,rdn_pos(rdn(rdnn(n6),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn16]) ).
cnf(f_17_2,plain,
rdn_translate(n16,rdn_pos(rdn(rdnn(n6),rdnn(n1)))),
inference(clausify,[status(thm)],[f_17_1]) ).
fof(f_18_1,plain,
rdn_translate(n17,rdn_pos(rdn(rdnn(n7),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn17]) ).
cnf(f_18_2,plain,
rdn_translate(n17,rdn_pos(rdn(rdnn(n7),rdnn(n1)))),
inference(clausify,[status(thm)],[f_18_1]) ).
fof(f_19_1,plain,
rdn_translate(n18,rdn_pos(rdn(rdnn(n8),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn18]) ).
cnf(f_19_2,plain,
rdn_translate(n18,rdn_pos(rdn(rdnn(n8),rdnn(n1)))),
inference(clausify,[status(thm)],[f_19_1]) ).
fof(f_20_1,plain,
rdn_translate(n19,rdn_pos(rdn(rdnn(n9),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdn19]) ).
cnf(f_20_2,plain,
rdn_translate(n19,rdn_pos(rdn(rdnn(n9),rdnn(n1)))),
inference(clausify,[status(thm)],[f_20_1]) ).
fof(f_21_1,plain,
rdn_translate(n20,rdn_pos(rdn(rdnn(n0),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn20]) ).
cnf(f_21_2,plain,
rdn_translate(n20,rdn_pos(rdn(rdnn(n0),rdnn(n2)))),
inference(clausify,[status(thm)],[f_21_1]) ).
fof(f_22_1,plain,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn21]) ).
cnf(f_22_2,plain,
rdn_translate(n21,rdn_pos(rdn(rdnn(n1),rdnn(n2)))),
inference(clausify,[status(thm)],[f_22_1]) ).
fof(f_23_1,plain,
rdn_translate(n22,rdn_pos(rdn(rdnn(n2),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn22]) ).
cnf(f_23_2,plain,
rdn_translate(n22,rdn_pos(rdn(rdnn(n2),rdnn(n2)))),
inference(clausify,[status(thm)],[f_23_1]) ).
fof(f_24_1,plain,
rdn_translate(n23,rdn_pos(rdn(rdnn(n3),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn23]) ).
cnf(f_24_2,plain,
rdn_translate(n23,rdn_pos(rdn(rdnn(n3),rdnn(n2)))),
inference(clausify,[status(thm)],[f_24_1]) ).
fof(f_25_1,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn24]) ).
cnf(f_25_2,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(clausify,[status(thm)],[f_25_1]) ).
fof(f_26_1,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn25]) ).
cnf(f_26_2,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(clausify,[status(thm)],[f_26_1]) ).
fof(f_27_1,plain,
rdn_translate(n26,rdn_pos(rdn(rdnn(n6),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn26]) ).
cnf(f_27_2,plain,
rdn_translate(n26,rdn_pos(rdn(rdnn(n6),rdnn(n2)))),
inference(clausify,[status(thm)],[f_27_1]) ).
fof(f_28_1,plain,
rdn_translate(n27,rdn_pos(rdn(rdnn(n7),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn27]) ).
cnf(f_28_2,plain,
rdn_translate(n27,rdn_pos(rdn(rdnn(n7),rdnn(n2)))),
inference(clausify,[status(thm)],[f_28_1]) ).
fof(f_29_1,plain,
rdn_translate(n28,rdn_pos(rdn(rdnn(n8),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn28]) ).
cnf(f_29_2,plain,
rdn_translate(n28,rdn_pos(rdn(rdnn(n8),rdnn(n2)))),
inference(clausify,[status(thm)],[f_29_1]) ).
fof(f_30_1,plain,
rdn_translate(n29,rdn_pos(rdn(rdnn(n9),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdn29]) ).
cnf(f_30_2,plain,
rdn_translate(n29,rdn_pos(rdn(rdnn(n9),rdnn(n2)))),
inference(clausify,[status(thm)],[f_30_1]) ).
fof(f_31_1,plain,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn30]) ).
cnf(f_31_2,plain,
rdn_translate(n30,rdn_pos(rdn(rdnn(n0),rdnn(n3)))),
inference(clausify,[status(thm)],[f_31_1]) ).
fof(f_32_1,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn31]) ).
cnf(f_32_2,plain,
rdn_translate(n31,rdn_pos(rdn(rdnn(n1),rdnn(n3)))),
inference(clausify,[status(thm)],[f_32_1]) ).
fof(f_33_1,plain,
rdn_translate(n32,rdn_pos(rdn(rdnn(n2),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn32]) ).
cnf(f_33_2,plain,
rdn_translate(n32,rdn_pos(rdn(rdnn(n2),rdnn(n3)))),
inference(clausify,[status(thm)],[f_33_1]) ).
fof(f_34_1,plain,
rdn_translate(n33,rdn_pos(rdn(rdnn(n3),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn33]) ).
cnf(f_34_2,plain,
rdn_translate(n33,rdn_pos(rdn(rdnn(n3),rdnn(n3)))),
inference(clausify,[status(thm)],[f_34_1]) ).
fof(f_35_1,plain,
rdn_translate(n34,rdn_pos(rdn(rdnn(n4),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn34]) ).
cnf(f_35_2,plain,
rdn_translate(n34,rdn_pos(rdn(rdnn(n4),rdnn(n3)))),
inference(clausify,[status(thm)],[f_35_1]) ).
fof(f_36_1,plain,
rdn_translate(n35,rdn_pos(rdn(rdnn(n5),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn35]) ).
cnf(f_36_2,plain,
rdn_translate(n35,rdn_pos(rdn(rdnn(n5),rdnn(n3)))),
inference(clausify,[status(thm)],[f_36_1]) ).
fof(f_37_1,plain,
rdn_translate(n36,rdn_pos(rdn(rdnn(n6),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn36]) ).
cnf(f_37_2,plain,
rdn_translate(n36,rdn_pos(rdn(rdnn(n6),rdnn(n3)))),
inference(clausify,[status(thm)],[f_37_1]) ).
fof(f_38_1,plain,
rdn_translate(n37,rdn_pos(rdn(rdnn(n7),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn37]) ).
cnf(f_38_2,plain,
rdn_translate(n37,rdn_pos(rdn(rdnn(n7),rdnn(n3)))),
inference(clausify,[status(thm)],[f_38_1]) ).
fof(f_39_1,plain,
rdn_translate(n38,rdn_pos(rdn(rdnn(n8),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn38]) ).
cnf(f_39_2,plain,
rdn_translate(n38,rdn_pos(rdn(rdnn(n8),rdnn(n3)))),
inference(clausify,[status(thm)],[f_39_1]) ).
fof(f_40_1,plain,
rdn_translate(n39,rdn_pos(rdn(rdnn(n9),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdn39]) ).
cnf(f_40_2,plain,
rdn_translate(n39,rdn_pos(rdn(rdnn(n9),rdnn(n3)))),
inference(clausify,[status(thm)],[f_40_1]) ).
fof(f_41_1,plain,
rdn_translate(n40,rdn_pos(rdn(rdnn(n0),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn40]) ).
cnf(f_41_2,plain,
rdn_translate(n40,rdn_pos(rdn(rdnn(n0),rdnn(n4)))),
inference(clausify,[status(thm)],[f_41_1]) ).
fof(f_42_1,plain,
rdn_translate(n41,rdn_pos(rdn(rdnn(n1),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn41]) ).
cnf(f_42_2,plain,
rdn_translate(n41,rdn_pos(rdn(rdnn(n1),rdnn(n4)))),
inference(clausify,[status(thm)],[f_42_1]) ).
fof(f_43_1,plain,
rdn_translate(n42,rdn_pos(rdn(rdnn(n2),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn42]) ).
cnf(f_43_2,plain,
rdn_translate(n42,rdn_pos(rdn(rdnn(n2),rdnn(n4)))),
inference(clausify,[status(thm)],[f_43_1]) ).
fof(f_44_1,plain,
rdn_translate(n43,rdn_pos(rdn(rdnn(n3),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn43]) ).
cnf(f_44_2,plain,
rdn_translate(n43,rdn_pos(rdn(rdnn(n3),rdnn(n4)))),
inference(clausify,[status(thm)],[f_44_1]) ).
fof(f_45_1,plain,
rdn_translate(n44,rdn_pos(rdn(rdnn(n4),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn44]) ).
cnf(f_45_2,plain,
rdn_translate(n44,rdn_pos(rdn(rdnn(n4),rdnn(n4)))),
inference(clausify,[status(thm)],[f_45_1]) ).
fof(f_46_1,plain,
rdn_translate(n45,rdn_pos(rdn(rdnn(n5),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn45]) ).
cnf(f_46_2,plain,
rdn_translate(n45,rdn_pos(rdn(rdnn(n5),rdnn(n4)))),
inference(clausify,[status(thm)],[f_46_1]) ).
fof(f_47_1,plain,
rdn_translate(n46,rdn_pos(rdn(rdnn(n6),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn46]) ).
cnf(f_47_2,plain,
rdn_translate(n46,rdn_pos(rdn(rdnn(n6),rdnn(n4)))),
inference(clausify,[status(thm)],[f_47_1]) ).
fof(f_48_1,plain,
rdn_translate(n47,rdn_pos(rdn(rdnn(n7),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn47]) ).
cnf(f_48_2,plain,
rdn_translate(n47,rdn_pos(rdn(rdnn(n7),rdnn(n4)))),
inference(clausify,[status(thm)],[f_48_1]) ).
fof(f_49_1,plain,
rdn_translate(n48,rdn_pos(rdn(rdnn(n8),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn48]) ).
cnf(f_49_2,plain,
rdn_translate(n48,rdn_pos(rdn(rdnn(n8),rdnn(n4)))),
inference(clausify,[status(thm)],[f_49_1]) ).
fof(f_50_1,plain,
rdn_translate(n49,rdn_pos(rdn(rdnn(n9),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdn49]) ).
cnf(f_50_2,plain,
rdn_translate(n49,rdn_pos(rdn(rdnn(n9),rdnn(n4)))),
inference(clausify,[status(thm)],[f_50_1]) ).
fof(f_51_1,plain,
rdn_translate(n50,rdn_pos(rdn(rdnn(n0),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn50]) ).
cnf(f_51_2,plain,
rdn_translate(n50,rdn_pos(rdn(rdnn(n0),rdnn(n5)))),
inference(clausify,[status(thm)],[f_51_1]) ).
fof(f_52_1,plain,
rdn_translate(n51,rdn_pos(rdn(rdnn(n1),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn51]) ).
cnf(f_52_2,plain,
rdn_translate(n51,rdn_pos(rdn(rdnn(n1),rdnn(n5)))),
inference(clausify,[status(thm)],[f_52_1]) ).
fof(f_53_1,plain,
rdn_translate(n52,rdn_pos(rdn(rdnn(n2),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn52]) ).
cnf(f_53_2,plain,
rdn_translate(n52,rdn_pos(rdn(rdnn(n2),rdnn(n5)))),
inference(clausify,[status(thm)],[f_53_1]) ).
fof(f_54_1,plain,
rdn_translate(n53,rdn_pos(rdn(rdnn(n3),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn53]) ).
cnf(f_54_2,plain,
rdn_translate(n53,rdn_pos(rdn(rdnn(n3),rdnn(n5)))),
inference(clausify,[status(thm)],[f_54_1]) ).
fof(f_55_1,plain,
rdn_translate(n54,rdn_pos(rdn(rdnn(n4),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn54]) ).
cnf(f_55_2,plain,
rdn_translate(n54,rdn_pos(rdn(rdnn(n4),rdnn(n5)))),
inference(clausify,[status(thm)],[f_55_1]) ).
fof(f_56_1,plain,
rdn_translate(n55,rdn_pos(rdn(rdnn(n5),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn55]) ).
cnf(f_56_2,plain,
rdn_translate(n55,rdn_pos(rdn(rdnn(n5),rdnn(n5)))),
inference(clausify,[status(thm)],[f_56_1]) ).
fof(f_57_1,plain,
rdn_translate(n56,rdn_pos(rdn(rdnn(n6),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn56]) ).
cnf(f_57_2,plain,
rdn_translate(n56,rdn_pos(rdn(rdnn(n6),rdnn(n5)))),
inference(clausify,[status(thm)],[f_57_1]) ).
fof(f_58_1,plain,
rdn_translate(n57,rdn_pos(rdn(rdnn(n7),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn57]) ).
cnf(f_58_2,plain,
rdn_translate(n57,rdn_pos(rdn(rdnn(n7),rdnn(n5)))),
inference(clausify,[status(thm)],[f_58_1]) ).
fof(f_59_1,plain,
rdn_translate(n58,rdn_pos(rdn(rdnn(n8),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn58]) ).
cnf(f_59_2,plain,
rdn_translate(n58,rdn_pos(rdn(rdnn(n8),rdnn(n5)))),
inference(clausify,[status(thm)],[f_59_1]) ).
fof(f_60_1,plain,
rdn_translate(n59,rdn_pos(rdn(rdnn(n9),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdn59]) ).
cnf(f_60_2,plain,
rdn_translate(n59,rdn_pos(rdn(rdnn(n9),rdnn(n5)))),
inference(clausify,[status(thm)],[f_60_1]) ).
fof(f_61_1,plain,
rdn_translate(n60,rdn_pos(rdn(rdnn(n0),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn60]) ).
cnf(f_61_2,plain,
rdn_translate(n60,rdn_pos(rdn(rdnn(n0),rdnn(n6)))),
inference(clausify,[status(thm)],[f_61_1]) ).
fof(f_62_1,plain,
rdn_translate(n61,rdn_pos(rdn(rdnn(n1),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn61]) ).
cnf(f_62_2,plain,
rdn_translate(n61,rdn_pos(rdn(rdnn(n1),rdnn(n6)))),
inference(clausify,[status(thm)],[f_62_1]) ).
fof(f_63_1,plain,
rdn_translate(n62,rdn_pos(rdn(rdnn(n2),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn62]) ).
cnf(f_63_2,plain,
rdn_translate(n62,rdn_pos(rdn(rdnn(n2),rdnn(n6)))),
inference(clausify,[status(thm)],[f_63_1]) ).
fof(f_64_1,plain,
rdn_translate(n63,rdn_pos(rdn(rdnn(n3),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn63]) ).
cnf(f_64_2,plain,
rdn_translate(n63,rdn_pos(rdn(rdnn(n3),rdnn(n6)))),
inference(clausify,[status(thm)],[f_64_1]) ).
fof(f_65_1,plain,
rdn_translate(n64,rdn_pos(rdn(rdnn(n4),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn64]) ).
cnf(f_65_2,plain,
rdn_translate(n64,rdn_pos(rdn(rdnn(n4),rdnn(n6)))),
inference(clausify,[status(thm)],[f_65_1]) ).
fof(f_66_1,plain,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn65]) ).
cnf(f_66_2,plain,
rdn_translate(n65,rdn_pos(rdn(rdnn(n5),rdnn(n6)))),
inference(clausify,[status(thm)],[f_66_1]) ).
fof(f_67_1,plain,
rdn_translate(n66,rdn_pos(rdn(rdnn(n6),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn66]) ).
cnf(f_67_2,plain,
rdn_translate(n66,rdn_pos(rdn(rdnn(n6),rdnn(n6)))),
inference(clausify,[status(thm)],[f_67_1]) ).
fof(f_68_1,plain,
rdn_translate(n67,rdn_pos(rdn(rdnn(n7),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn67]) ).
cnf(f_68_2,plain,
rdn_translate(n67,rdn_pos(rdn(rdnn(n7),rdnn(n6)))),
inference(clausify,[status(thm)],[f_68_1]) ).
fof(f_69_1,plain,
rdn_translate(n68,rdn_pos(rdn(rdnn(n8),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn68]) ).
cnf(f_69_2,plain,
rdn_translate(n68,rdn_pos(rdn(rdnn(n8),rdnn(n6)))),
inference(clausify,[status(thm)],[f_69_1]) ).
fof(f_70_1,plain,
rdn_translate(n69,rdn_pos(rdn(rdnn(n9),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdn69]) ).
cnf(f_70_2,plain,
rdn_translate(n69,rdn_pos(rdn(rdnn(n9),rdnn(n6)))),
inference(clausify,[status(thm)],[f_70_1]) ).
fof(f_71_1,plain,
rdn_translate(n70,rdn_pos(rdn(rdnn(n0),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn70]) ).
cnf(f_71_2,plain,
rdn_translate(n70,rdn_pos(rdn(rdnn(n0),rdnn(n7)))),
inference(clausify,[status(thm)],[f_71_1]) ).
fof(f_72_1,plain,
rdn_translate(n71,rdn_pos(rdn(rdnn(n1),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn71]) ).
cnf(f_72_2,plain,
rdn_translate(n71,rdn_pos(rdn(rdnn(n1),rdnn(n7)))),
inference(clausify,[status(thm)],[f_72_1]) ).
fof(f_73_1,plain,
rdn_translate(n72,rdn_pos(rdn(rdnn(n2),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn72]) ).
cnf(f_73_2,plain,
rdn_translate(n72,rdn_pos(rdn(rdnn(n2),rdnn(n7)))),
inference(clausify,[status(thm)],[f_73_1]) ).
fof(f_74_1,plain,
rdn_translate(n73,rdn_pos(rdn(rdnn(n3),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn73]) ).
cnf(f_74_2,plain,
rdn_translate(n73,rdn_pos(rdn(rdnn(n3),rdnn(n7)))),
inference(clausify,[status(thm)],[f_74_1]) ).
fof(f_75_1,plain,
rdn_translate(n74,rdn_pos(rdn(rdnn(n4),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn74]) ).
cnf(f_75_2,plain,
rdn_translate(n74,rdn_pos(rdn(rdnn(n4),rdnn(n7)))),
inference(clausify,[status(thm)],[f_75_1]) ).
fof(f_76_1,plain,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn75]) ).
cnf(f_76_2,plain,
rdn_translate(n75,rdn_pos(rdn(rdnn(n5),rdnn(n7)))),
inference(clausify,[status(thm)],[f_76_1]) ).
fof(f_77_1,plain,
rdn_translate(n76,rdn_pos(rdn(rdnn(n6),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn76]) ).
cnf(f_77_2,plain,
rdn_translate(n76,rdn_pos(rdn(rdnn(n6),rdnn(n7)))),
inference(clausify,[status(thm)],[f_77_1]) ).
fof(f_78_1,plain,
rdn_translate(n77,rdn_pos(rdn(rdnn(n7),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn77]) ).
cnf(f_78_2,plain,
rdn_translate(n77,rdn_pos(rdn(rdnn(n7),rdnn(n7)))),
inference(clausify,[status(thm)],[f_78_1]) ).
fof(f_79_1,plain,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn78]) ).
cnf(f_79_2,plain,
rdn_translate(n78,rdn_pos(rdn(rdnn(n8),rdnn(n7)))),
inference(clausify,[status(thm)],[f_79_1]) ).
fof(f_80_1,plain,
rdn_translate(n79,rdn_pos(rdn(rdnn(n9),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdn79]) ).
cnf(f_80_2,plain,
rdn_translate(n79,rdn_pos(rdn(rdnn(n9),rdnn(n7)))),
inference(clausify,[status(thm)],[f_80_1]) ).
fof(f_81_1,plain,
rdn_translate(n80,rdn_pos(rdn(rdnn(n0),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn80]) ).
cnf(f_81_2,plain,
rdn_translate(n80,rdn_pos(rdn(rdnn(n0),rdnn(n8)))),
inference(clausify,[status(thm)],[f_81_1]) ).
fof(f_82_1,plain,
rdn_translate(n81,rdn_pos(rdn(rdnn(n1),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn81]) ).
cnf(f_82_2,plain,
rdn_translate(n81,rdn_pos(rdn(rdnn(n1),rdnn(n8)))),
inference(clausify,[status(thm)],[f_82_1]) ).
fof(f_83_1,plain,
rdn_translate(n82,rdn_pos(rdn(rdnn(n2),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn82]) ).
cnf(f_83_2,plain,
rdn_translate(n82,rdn_pos(rdn(rdnn(n2),rdnn(n8)))),
inference(clausify,[status(thm)],[f_83_1]) ).
fof(f_84_1,plain,
rdn_translate(n83,rdn_pos(rdn(rdnn(n3),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn83]) ).
cnf(f_84_2,plain,
rdn_translate(n83,rdn_pos(rdn(rdnn(n3),rdnn(n8)))),
inference(clausify,[status(thm)],[f_84_1]) ).
fof(f_85_1,plain,
rdn_translate(n84,rdn_pos(rdn(rdnn(n4),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn84]) ).
cnf(f_85_2,plain,
rdn_translate(n84,rdn_pos(rdn(rdnn(n4),rdnn(n8)))),
inference(clausify,[status(thm)],[f_85_1]) ).
fof(f_86_1,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn85]) ).
cnf(f_86_2,plain,
rdn_translate(n85,rdn_pos(rdn(rdnn(n5),rdnn(n8)))),
inference(clausify,[status(thm)],[f_86_1]) ).
fof(f_87_1,plain,
rdn_translate(n86,rdn_pos(rdn(rdnn(n6),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn86]) ).
cnf(f_87_2,plain,
rdn_translate(n86,rdn_pos(rdn(rdnn(n6),rdnn(n8)))),
inference(clausify,[status(thm)],[f_87_1]) ).
fof(f_88_1,plain,
rdn_translate(n87,rdn_pos(rdn(rdnn(n7),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn87]) ).
cnf(f_88_2,plain,
rdn_translate(n87,rdn_pos(rdn(rdnn(n7),rdnn(n8)))),
inference(clausify,[status(thm)],[f_88_1]) ).
fof(f_89_1,plain,
rdn_translate(n88,rdn_pos(rdn(rdnn(n8),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn88]) ).
cnf(f_89_2,plain,
rdn_translate(n88,rdn_pos(rdn(rdnn(n8),rdnn(n8)))),
inference(clausify,[status(thm)],[f_89_1]) ).
fof(f_90_1,plain,
rdn_translate(n89,rdn_pos(rdn(rdnn(n9),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdn89]) ).
cnf(f_90_2,plain,
rdn_translate(n89,rdn_pos(rdn(rdnn(n9),rdnn(n8)))),
inference(clausify,[status(thm)],[f_90_1]) ).
fof(f_91_1,plain,
rdn_translate(n90,rdn_pos(rdn(rdnn(n0),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn90]) ).
cnf(f_91_2,plain,
rdn_translate(n90,rdn_pos(rdn(rdnn(n0),rdnn(n9)))),
inference(clausify,[status(thm)],[f_91_1]) ).
fof(f_92_1,plain,
rdn_translate(n91,rdn_pos(rdn(rdnn(n1),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn91]) ).
cnf(f_92_2,plain,
rdn_translate(n91,rdn_pos(rdn(rdnn(n1),rdnn(n9)))),
inference(clausify,[status(thm)],[f_92_1]) ).
fof(f_93_1,plain,
rdn_translate(n92,rdn_pos(rdn(rdnn(n2),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn92]) ).
cnf(f_93_2,plain,
rdn_translate(n92,rdn_pos(rdn(rdnn(n2),rdnn(n9)))),
inference(clausify,[status(thm)],[f_93_1]) ).
fof(f_94_1,plain,
rdn_translate(n93,rdn_pos(rdn(rdnn(n3),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn93]) ).
cnf(f_94_2,plain,
rdn_translate(n93,rdn_pos(rdn(rdnn(n3),rdnn(n9)))),
inference(clausify,[status(thm)],[f_94_1]) ).
fof(f_95_1,plain,
rdn_translate(n94,rdn_pos(rdn(rdnn(n4),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn94]) ).
cnf(f_95_2,plain,
rdn_translate(n94,rdn_pos(rdn(rdnn(n4),rdnn(n9)))),
inference(clausify,[status(thm)],[f_95_1]) ).
fof(f_96_1,plain,
rdn_translate(n95,rdn_pos(rdn(rdnn(n5),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn95]) ).
cnf(f_96_2,plain,
rdn_translate(n95,rdn_pos(rdn(rdnn(n5),rdnn(n9)))),
inference(clausify,[status(thm)],[f_96_1]) ).
fof(f_97_1,plain,
rdn_translate(n96,rdn_pos(rdn(rdnn(n6),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn96]) ).
cnf(f_97_2,plain,
rdn_translate(n96,rdn_pos(rdn(rdnn(n6),rdnn(n9)))),
inference(clausify,[status(thm)],[f_97_1]) ).
fof(f_98_1,plain,
rdn_translate(n97,rdn_pos(rdn(rdnn(n7),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn97]) ).
cnf(f_98_2,plain,
rdn_translate(n97,rdn_pos(rdn(rdnn(n7),rdnn(n9)))),
inference(clausify,[status(thm)],[f_98_1]) ).
fof(f_99_1,plain,
rdn_translate(n98,rdn_pos(rdn(rdnn(n8),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn98]) ).
cnf(f_99_2,plain,
rdn_translate(n98,rdn_pos(rdn(rdnn(n8),rdnn(n9)))),
inference(clausify,[status(thm)],[f_99_1]) ).
fof(f_100_1,plain,
rdn_translate(n99,rdn_pos(rdn(rdnn(n9),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdn99]) ).
cnf(f_100_2,plain,
rdn_translate(n99,rdn_pos(rdn(rdnn(n9),rdnn(n9)))),
inference(clausify,[status(thm)],[f_100_1]) ).
fof(f_101_1,plain,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn100]) ).
cnf(f_101_2,plain,
rdn_translate(n100,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_101_1]) ).
fof(f_102_1,plain,
rdn_translate(n101,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn101]) ).
cnf(f_102_2,plain,
rdn_translate(n101,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_102_1]) ).
fof(f_103_1,plain,
rdn_translate(n102,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn102]) ).
cnf(f_103_2,plain,
rdn_translate(n102,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_103_1]) ).
fof(f_104_1,plain,
rdn_translate(n103,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn103]) ).
cnf(f_104_2,plain,
rdn_translate(n103,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_104_1]) ).
fof(f_105_1,plain,
rdn_translate(n104,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn104]) ).
cnf(f_105_2,plain,
rdn_translate(n104,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_105_1]) ).
fof(f_106_1,plain,
rdn_translate(n105,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn105]) ).
cnf(f_106_2,plain,
rdn_translate(n105,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_106_1]) ).
fof(f_107_1,plain,
rdn_translate(n106,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn106]) ).
cnf(f_107_2,plain,
rdn_translate(n106,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_107_1]) ).
fof(f_108_1,plain,
rdn_translate(n107,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn107]) ).
cnf(f_108_2,plain,
rdn_translate(n107,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_108_1]) ).
fof(f_109_1,plain,
rdn_translate(n108,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn108]) ).
cnf(f_109_2,plain,
rdn_translate(n108,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_109_1]) ).
fof(f_110_1,plain,
rdn_translate(n109,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn109]) ).
cnf(f_110_2,plain,
rdn_translate(n109,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_110_1]) ).
fof(f_111_1,plain,
rdn_translate(n110,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn110]) ).
cnf(f_111_2,plain,
rdn_translate(n110,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_111_1]) ).
fof(f_112_1,plain,
rdn_translate(n111,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn111]) ).
cnf(f_112_2,plain,
rdn_translate(n111,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_112_1]) ).
fof(f_113_1,plain,
rdn_translate(n112,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn112]) ).
cnf(f_113_2,plain,
rdn_translate(n112,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_113_1]) ).
fof(f_114_1,plain,
rdn_translate(n113,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn113]) ).
cnf(f_114_2,plain,
rdn_translate(n113,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_114_1]) ).
fof(f_115_1,plain,
rdn_translate(n114,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn114]) ).
cnf(f_115_2,plain,
rdn_translate(n114,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_115_1]) ).
fof(f_116_1,plain,
rdn_translate(n115,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn115]) ).
cnf(f_116_2,plain,
rdn_translate(n115,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_116_1]) ).
fof(f_117_1,plain,
rdn_translate(n116,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn116]) ).
cnf(f_117_2,plain,
rdn_translate(n116,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_117_1]) ).
fof(f_118_1,plain,
rdn_translate(n117,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn117]) ).
cnf(f_118_2,plain,
rdn_translate(n117,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_118_1]) ).
fof(f_119_1,plain,
rdn_translate(n118,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn118]) ).
cnf(f_119_2,plain,
rdn_translate(n118,rdn_pos(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_119_1]) ).
fof(f_120_1,plain,
rdn_translate(n119,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn119]) ).
cnf(f_120_2,plain,
rdn_translate(n119,rdn_pos(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_120_1]) ).
fof(f_121_1,plain,
rdn_translate(n120,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn120]) ).
cnf(f_121_2,plain,
rdn_translate(n120,rdn_pos(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_121_1]) ).
fof(f_122_1,plain,
rdn_translate(n121,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn121]) ).
cnf(f_122_2,plain,
rdn_translate(n121,rdn_pos(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_122_1]) ).
fof(f_123_1,plain,
rdn_translate(n122,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn122]) ).
cnf(f_123_2,plain,
rdn_translate(n122,rdn_pos(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_123_1]) ).
fof(f_124_1,plain,
rdn_translate(n123,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn123]) ).
cnf(f_124_2,plain,
rdn_translate(n123,rdn_pos(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_124_1]) ).
fof(f_125_1,plain,
rdn_translate(n124,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn124]) ).
cnf(f_125_2,plain,
rdn_translate(n124,rdn_pos(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_125_1]) ).
fof(f_126_1,plain,
rdn_translate(n125,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn125]) ).
cnf(f_126_2,plain,
rdn_translate(n125,rdn_pos(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_126_1]) ).
fof(f_127_1,plain,
rdn_translate(n126,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn126]) ).
cnf(f_127_2,plain,
rdn_translate(n126,rdn_pos(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_127_1]) ).
fof(f_128_1,plain,
rdn_translate(n127,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdn127]) ).
cnf(f_128_2,plain,
rdn_translate(n127,rdn_pos(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_128_1]) ).
fof(f_129_1,plain,
rdn_translate(nn1,rdn_neg(rdnn(n1))),
inference(fof_nnf,[status(thm)],[rdnn1]) ).
cnf(f_129_2,plain,
rdn_translate(nn1,rdn_neg(rdnn(n1))),
inference(clausify,[status(thm)],[f_129_1]) ).
fof(f_130_1,plain,
rdn_translate(nn2,rdn_neg(rdnn(n2))),
inference(fof_nnf,[status(thm)],[rdnn2]) ).
cnf(f_130_2,plain,
rdn_translate(nn2,rdn_neg(rdnn(n2))),
inference(clausify,[status(thm)],[f_130_1]) ).
fof(f_131_1,plain,
rdn_translate(nn3,rdn_neg(rdnn(n3))),
inference(fof_nnf,[status(thm)],[rdnn3]) ).
cnf(f_131_2,plain,
rdn_translate(nn3,rdn_neg(rdnn(n3))),
inference(clausify,[status(thm)],[f_131_1]) ).
fof(f_132_1,plain,
rdn_translate(nn4,rdn_neg(rdnn(n4))),
inference(fof_nnf,[status(thm)],[rdnn4]) ).
cnf(f_132_2,plain,
rdn_translate(nn4,rdn_neg(rdnn(n4))),
inference(clausify,[status(thm)],[f_132_1]) ).
fof(f_133_1,plain,
rdn_translate(nn5,rdn_neg(rdnn(n5))),
inference(fof_nnf,[status(thm)],[rdnn5]) ).
cnf(f_133_2,plain,
rdn_translate(nn5,rdn_neg(rdnn(n5))),
inference(clausify,[status(thm)],[f_133_1]) ).
fof(f_134_1,plain,
rdn_translate(nn6,rdn_neg(rdnn(n6))),
inference(fof_nnf,[status(thm)],[rdnn6]) ).
cnf(f_134_2,plain,
rdn_translate(nn6,rdn_neg(rdnn(n6))),
inference(clausify,[status(thm)],[f_134_1]) ).
fof(f_135_1,plain,
rdn_translate(nn7,rdn_neg(rdnn(n7))),
inference(fof_nnf,[status(thm)],[rdnn7]) ).
cnf(f_135_2,plain,
rdn_translate(nn7,rdn_neg(rdnn(n7))),
inference(clausify,[status(thm)],[f_135_1]) ).
fof(f_136_1,plain,
rdn_translate(nn8,rdn_neg(rdnn(n8))),
inference(fof_nnf,[status(thm)],[rdnn8]) ).
cnf(f_136_2,plain,
rdn_translate(nn8,rdn_neg(rdnn(n8))),
inference(clausify,[status(thm)],[f_136_1]) ).
fof(f_137_1,plain,
rdn_translate(nn9,rdn_neg(rdnn(n9))),
inference(fof_nnf,[status(thm)],[rdnn9]) ).
cnf(f_137_2,plain,
rdn_translate(nn9,rdn_neg(rdnn(n9))),
inference(clausify,[status(thm)],[f_137_1]) ).
fof(f_138_1,plain,
rdn_translate(nn10,rdn_neg(rdn(rdnn(n0),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn10]) ).
cnf(f_138_2,plain,
rdn_translate(nn10,rdn_neg(rdn(rdnn(n0),rdnn(n1)))),
inference(clausify,[status(thm)],[f_138_1]) ).
fof(f_139_1,plain,
rdn_translate(nn11,rdn_neg(rdn(rdnn(n1),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn11]) ).
cnf(f_139_2,plain,
rdn_translate(nn11,rdn_neg(rdn(rdnn(n1),rdnn(n1)))),
inference(clausify,[status(thm)],[f_139_1]) ).
fof(f_140_1,plain,
rdn_translate(nn12,rdn_neg(rdn(rdnn(n2),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn12]) ).
cnf(f_140_2,plain,
rdn_translate(nn12,rdn_neg(rdn(rdnn(n2),rdnn(n1)))),
inference(clausify,[status(thm)],[f_140_1]) ).
fof(f_141_1,plain,
rdn_translate(nn13,rdn_neg(rdn(rdnn(n3),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn13]) ).
cnf(f_141_2,plain,
rdn_translate(nn13,rdn_neg(rdn(rdnn(n3),rdnn(n1)))),
inference(clausify,[status(thm)],[f_141_1]) ).
fof(f_142_1,plain,
rdn_translate(nn14,rdn_neg(rdn(rdnn(n4),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn14]) ).
cnf(f_142_2,plain,
rdn_translate(nn14,rdn_neg(rdn(rdnn(n4),rdnn(n1)))),
inference(clausify,[status(thm)],[f_142_1]) ).
fof(f_143_1,plain,
rdn_translate(nn15,rdn_neg(rdn(rdnn(n5),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn15]) ).
cnf(f_143_2,plain,
rdn_translate(nn15,rdn_neg(rdn(rdnn(n5),rdnn(n1)))),
inference(clausify,[status(thm)],[f_143_1]) ).
fof(f_144_1,plain,
rdn_translate(nn16,rdn_neg(rdn(rdnn(n6),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn16]) ).
cnf(f_144_2,plain,
rdn_translate(nn16,rdn_neg(rdn(rdnn(n6),rdnn(n1)))),
inference(clausify,[status(thm)],[f_144_1]) ).
fof(f_145_1,plain,
rdn_translate(nn17,rdn_neg(rdn(rdnn(n7),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn17]) ).
cnf(f_145_2,plain,
rdn_translate(nn17,rdn_neg(rdn(rdnn(n7),rdnn(n1)))),
inference(clausify,[status(thm)],[f_145_1]) ).
fof(f_146_1,plain,
rdn_translate(nn18,rdn_neg(rdn(rdnn(n8),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn18]) ).
cnf(f_146_2,plain,
rdn_translate(nn18,rdn_neg(rdn(rdnn(n8),rdnn(n1)))),
inference(clausify,[status(thm)],[f_146_1]) ).
fof(f_147_1,plain,
rdn_translate(nn19,rdn_neg(rdn(rdnn(n9),rdnn(n1)))),
inference(fof_nnf,[status(thm)],[rdnn19]) ).
cnf(f_147_2,plain,
rdn_translate(nn19,rdn_neg(rdn(rdnn(n9),rdnn(n1)))),
inference(clausify,[status(thm)],[f_147_1]) ).
fof(f_148_1,plain,
rdn_translate(nn20,rdn_neg(rdn(rdnn(n0),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn20]) ).
cnf(f_148_2,plain,
rdn_translate(nn20,rdn_neg(rdn(rdnn(n0),rdnn(n2)))),
inference(clausify,[status(thm)],[f_148_1]) ).
fof(f_149_1,plain,
rdn_translate(nn21,rdn_neg(rdn(rdnn(n1),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn21]) ).
cnf(f_149_2,plain,
rdn_translate(nn21,rdn_neg(rdn(rdnn(n1),rdnn(n2)))),
inference(clausify,[status(thm)],[f_149_1]) ).
fof(f_150_1,plain,
rdn_translate(nn22,rdn_neg(rdn(rdnn(n2),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn22]) ).
cnf(f_150_2,plain,
rdn_translate(nn22,rdn_neg(rdn(rdnn(n2),rdnn(n2)))),
inference(clausify,[status(thm)],[f_150_1]) ).
fof(f_151_1,plain,
rdn_translate(nn23,rdn_neg(rdn(rdnn(n3),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn23]) ).
cnf(f_151_2,plain,
rdn_translate(nn23,rdn_neg(rdn(rdnn(n3),rdnn(n2)))),
inference(clausify,[status(thm)],[f_151_1]) ).
fof(f_152_1,plain,
rdn_translate(nn24,rdn_neg(rdn(rdnn(n4),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn24]) ).
cnf(f_152_2,plain,
rdn_translate(nn24,rdn_neg(rdn(rdnn(n4),rdnn(n2)))),
inference(clausify,[status(thm)],[f_152_1]) ).
fof(f_153_1,plain,
rdn_translate(nn25,rdn_neg(rdn(rdnn(n5),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn25]) ).
cnf(f_153_2,plain,
rdn_translate(nn25,rdn_neg(rdn(rdnn(n5),rdnn(n2)))),
inference(clausify,[status(thm)],[f_153_1]) ).
fof(f_154_1,plain,
rdn_translate(nn26,rdn_neg(rdn(rdnn(n6),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn26]) ).
cnf(f_154_2,plain,
rdn_translate(nn26,rdn_neg(rdn(rdnn(n6),rdnn(n2)))),
inference(clausify,[status(thm)],[f_154_1]) ).
fof(f_155_1,plain,
rdn_translate(nn27,rdn_neg(rdn(rdnn(n7),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn27]) ).
cnf(f_155_2,plain,
rdn_translate(nn27,rdn_neg(rdn(rdnn(n7),rdnn(n2)))),
inference(clausify,[status(thm)],[f_155_1]) ).
fof(f_156_1,plain,
rdn_translate(nn28,rdn_neg(rdn(rdnn(n8),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn28]) ).
cnf(f_156_2,plain,
rdn_translate(nn28,rdn_neg(rdn(rdnn(n8),rdnn(n2)))),
inference(clausify,[status(thm)],[f_156_1]) ).
fof(f_157_1,plain,
rdn_translate(nn29,rdn_neg(rdn(rdnn(n9),rdnn(n2)))),
inference(fof_nnf,[status(thm)],[rdnn29]) ).
cnf(f_157_2,plain,
rdn_translate(nn29,rdn_neg(rdn(rdnn(n9),rdnn(n2)))),
inference(clausify,[status(thm)],[f_157_1]) ).
fof(f_158_1,plain,
rdn_translate(nn30,rdn_neg(rdn(rdnn(n0),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn30]) ).
cnf(f_158_2,plain,
rdn_translate(nn30,rdn_neg(rdn(rdnn(n0),rdnn(n3)))),
inference(clausify,[status(thm)],[f_158_1]) ).
fof(f_159_1,plain,
rdn_translate(nn31,rdn_neg(rdn(rdnn(n1),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn31]) ).
cnf(f_159_2,plain,
rdn_translate(nn31,rdn_neg(rdn(rdnn(n1),rdnn(n3)))),
inference(clausify,[status(thm)],[f_159_1]) ).
fof(f_160_1,plain,
rdn_translate(nn32,rdn_neg(rdn(rdnn(n2),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn32]) ).
cnf(f_160_2,plain,
rdn_translate(nn32,rdn_neg(rdn(rdnn(n2),rdnn(n3)))),
inference(clausify,[status(thm)],[f_160_1]) ).
fof(f_161_1,plain,
rdn_translate(nn33,rdn_neg(rdn(rdnn(n3),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn33]) ).
cnf(f_161_2,plain,
rdn_translate(nn33,rdn_neg(rdn(rdnn(n3),rdnn(n3)))),
inference(clausify,[status(thm)],[f_161_1]) ).
fof(f_162_1,plain,
rdn_translate(nn34,rdn_neg(rdn(rdnn(n4),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn34]) ).
cnf(f_162_2,plain,
rdn_translate(nn34,rdn_neg(rdn(rdnn(n4),rdnn(n3)))),
inference(clausify,[status(thm)],[f_162_1]) ).
fof(f_163_1,plain,
rdn_translate(nn35,rdn_neg(rdn(rdnn(n5),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn35]) ).
cnf(f_163_2,plain,
rdn_translate(nn35,rdn_neg(rdn(rdnn(n5),rdnn(n3)))),
inference(clausify,[status(thm)],[f_163_1]) ).
fof(f_164_1,plain,
rdn_translate(nn36,rdn_neg(rdn(rdnn(n6),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn36]) ).
cnf(f_164_2,plain,
rdn_translate(nn36,rdn_neg(rdn(rdnn(n6),rdnn(n3)))),
inference(clausify,[status(thm)],[f_164_1]) ).
fof(f_165_1,plain,
rdn_translate(nn37,rdn_neg(rdn(rdnn(n7),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn37]) ).
cnf(f_165_2,plain,
rdn_translate(nn37,rdn_neg(rdn(rdnn(n7),rdnn(n3)))),
inference(clausify,[status(thm)],[f_165_1]) ).
fof(f_166_1,plain,
rdn_translate(nn38,rdn_neg(rdn(rdnn(n8),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn38]) ).
cnf(f_166_2,plain,
rdn_translate(nn38,rdn_neg(rdn(rdnn(n8),rdnn(n3)))),
inference(clausify,[status(thm)],[f_166_1]) ).
fof(f_167_1,plain,
rdn_translate(nn39,rdn_neg(rdn(rdnn(n9),rdnn(n3)))),
inference(fof_nnf,[status(thm)],[rdnn39]) ).
cnf(f_167_2,plain,
rdn_translate(nn39,rdn_neg(rdn(rdnn(n9),rdnn(n3)))),
inference(clausify,[status(thm)],[f_167_1]) ).
fof(f_168_1,plain,
rdn_translate(nn40,rdn_neg(rdn(rdnn(n0),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn40]) ).
cnf(f_168_2,plain,
rdn_translate(nn40,rdn_neg(rdn(rdnn(n0),rdnn(n4)))),
inference(clausify,[status(thm)],[f_168_1]) ).
fof(f_169_1,plain,
rdn_translate(nn41,rdn_neg(rdn(rdnn(n1),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn41]) ).
cnf(f_169_2,plain,
rdn_translate(nn41,rdn_neg(rdn(rdnn(n1),rdnn(n4)))),
inference(clausify,[status(thm)],[f_169_1]) ).
fof(f_170_1,plain,
rdn_translate(nn42,rdn_neg(rdn(rdnn(n2),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn42]) ).
cnf(f_170_2,plain,
rdn_translate(nn42,rdn_neg(rdn(rdnn(n2),rdnn(n4)))),
inference(clausify,[status(thm)],[f_170_1]) ).
fof(f_171_1,plain,
rdn_translate(nn43,rdn_neg(rdn(rdnn(n3),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn43]) ).
cnf(f_171_2,plain,
rdn_translate(nn43,rdn_neg(rdn(rdnn(n3),rdnn(n4)))),
inference(clausify,[status(thm)],[f_171_1]) ).
fof(f_172_1,plain,
rdn_translate(nn44,rdn_neg(rdn(rdnn(n4),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn44]) ).
cnf(f_172_2,plain,
rdn_translate(nn44,rdn_neg(rdn(rdnn(n4),rdnn(n4)))),
inference(clausify,[status(thm)],[f_172_1]) ).
fof(f_173_1,plain,
rdn_translate(nn45,rdn_neg(rdn(rdnn(n5),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn45]) ).
cnf(f_173_2,plain,
rdn_translate(nn45,rdn_neg(rdn(rdnn(n5),rdnn(n4)))),
inference(clausify,[status(thm)],[f_173_1]) ).
fof(f_174_1,plain,
rdn_translate(nn46,rdn_neg(rdn(rdnn(n6),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn46]) ).
cnf(f_174_2,plain,
rdn_translate(nn46,rdn_neg(rdn(rdnn(n6),rdnn(n4)))),
inference(clausify,[status(thm)],[f_174_1]) ).
fof(f_175_1,plain,
rdn_translate(nn47,rdn_neg(rdn(rdnn(n7),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn47]) ).
cnf(f_175_2,plain,
rdn_translate(nn47,rdn_neg(rdn(rdnn(n7),rdnn(n4)))),
inference(clausify,[status(thm)],[f_175_1]) ).
fof(f_176_1,plain,
rdn_translate(nn48,rdn_neg(rdn(rdnn(n8),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn48]) ).
cnf(f_176_2,plain,
rdn_translate(nn48,rdn_neg(rdn(rdnn(n8),rdnn(n4)))),
inference(clausify,[status(thm)],[f_176_1]) ).
fof(f_177_1,plain,
rdn_translate(nn49,rdn_neg(rdn(rdnn(n9),rdnn(n4)))),
inference(fof_nnf,[status(thm)],[rdnn49]) ).
cnf(f_177_2,plain,
rdn_translate(nn49,rdn_neg(rdn(rdnn(n9),rdnn(n4)))),
inference(clausify,[status(thm)],[f_177_1]) ).
fof(f_178_1,plain,
rdn_translate(nn50,rdn_neg(rdn(rdnn(n0),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn50]) ).
cnf(f_178_2,plain,
rdn_translate(nn50,rdn_neg(rdn(rdnn(n0),rdnn(n5)))),
inference(clausify,[status(thm)],[f_178_1]) ).
fof(f_179_1,plain,
rdn_translate(nn51,rdn_neg(rdn(rdnn(n1),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn51]) ).
cnf(f_179_2,plain,
rdn_translate(nn51,rdn_neg(rdn(rdnn(n1),rdnn(n5)))),
inference(clausify,[status(thm)],[f_179_1]) ).
fof(f_180_1,plain,
rdn_translate(nn52,rdn_neg(rdn(rdnn(n2),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn52]) ).
cnf(f_180_2,plain,
rdn_translate(nn52,rdn_neg(rdn(rdnn(n2),rdnn(n5)))),
inference(clausify,[status(thm)],[f_180_1]) ).
fof(f_181_1,plain,
rdn_translate(nn53,rdn_neg(rdn(rdnn(n3),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn53]) ).
cnf(f_181_2,plain,
rdn_translate(nn53,rdn_neg(rdn(rdnn(n3),rdnn(n5)))),
inference(clausify,[status(thm)],[f_181_1]) ).
fof(f_182_1,plain,
rdn_translate(nn54,rdn_neg(rdn(rdnn(n4),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn54]) ).
cnf(f_182_2,plain,
rdn_translate(nn54,rdn_neg(rdn(rdnn(n4),rdnn(n5)))),
inference(clausify,[status(thm)],[f_182_1]) ).
fof(f_183_1,plain,
rdn_translate(nn55,rdn_neg(rdn(rdnn(n5),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn55]) ).
cnf(f_183_2,plain,
rdn_translate(nn55,rdn_neg(rdn(rdnn(n5),rdnn(n5)))),
inference(clausify,[status(thm)],[f_183_1]) ).
fof(f_184_1,plain,
rdn_translate(nn56,rdn_neg(rdn(rdnn(n6),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn56]) ).
cnf(f_184_2,plain,
rdn_translate(nn56,rdn_neg(rdn(rdnn(n6),rdnn(n5)))),
inference(clausify,[status(thm)],[f_184_1]) ).
fof(f_185_1,plain,
rdn_translate(nn57,rdn_neg(rdn(rdnn(n7),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn57]) ).
cnf(f_185_2,plain,
rdn_translate(nn57,rdn_neg(rdn(rdnn(n7),rdnn(n5)))),
inference(clausify,[status(thm)],[f_185_1]) ).
fof(f_186_1,plain,
rdn_translate(nn58,rdn_neg(rdn(rdnn(n8),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn58]) ).
cnf(f_186_2,plain,
rdn_translate(nn58,rdn_neg(rdn(rdnn(n8),rdnn(n5)))),
inference(clausify,[status(thm)],[f_186_1]) ).
fof(f_187_1,plain,
rdn_translate(nn59,rdn_neg(rdn(rdnn(n9),rdnn(n5)))),
inference(fof_nnf,[status(thm)],[rdnn59]) ).
cnf(f_187_2,plain,
rdn_translate(nn59,rdn_neg(rdn(rdnn(n9),rdnn(n5)))),
inference(clausify,[status(thm)],[f_187_1]) ).
fof(f_188_1,plain,
rdn_translate(nn60,rdn_neg(rdn(rdnn(n0),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn60]) ).
cnf(f_188_2,plain,
rdn_translate(nn60,rdn_neg(rdn(rdnn(n0),rdnn(n6)))),
inference(clausify,[status(thm)],[f_188_1]) ).
fof(f_189_1,plain,
rdn_translate(nn61,rdn_neg(rdn(rdnn(n1),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn61]) ).
cnf(f_189_2,plain,
rdn_translate(nn61,rdn_neg(rdn(rdnn(n1),rdnn(n6)))),
inference(clausify,[status(thm)],[f_189_1]) ).
fof(f_190_1,plain,
rdn_translate(nn62,rdn_neg(rdn(rdnn(n2),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn62]) ).
cnf(f_190_2,plain,
rdn_translate(nn62,rdn_neg(rdn(rdnn(n2),rdnn(n6)))),
inference(clausify,[status(thm)],[f_190_1]) ).
fof(f_191_1,plain,
rdn_translate(nn63,rdn_neg(rdn(rdnn(n3),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn63]) ).
cnf(f_191_2,plain,
rdn_translate(nn63,rdn_neg(rdn(rdnn(n3),rdnn(n6)))),
inference(clausify,[status(thm)],[f_191_1]) ).
fof(f_192_1,plain,
rdn_translate(nn64,rdn_neg(rdn(rdnn(n4),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn64]) ).
cnf(f_192_2,plain,
rdn_translate(nn64,rdn_neg(rdn(rdnn(n4),rdnn(n6)))),
inference(clausify,[status(thm)],[f_192_1]) ).
fof(f_193_1,plain,
rdn_translate(nn65,rdn_neg(rdn(rdnn(n5),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn65]) ).
cnf(f_193_2,plain,
rdn_translate(nn65,rdn_neg(rdn(rdnn(n5),rdnn(n6)))),
inference(clausify,[status(thm)],[f_193_1]) ).
fof(f_194_1,plain,
rdn_translate(nn66,rdn_neg(rdn(rdnn(n6),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn66]) ).
cnf(f_194_2,plain,
rdn_translate(nn66,rdn_neg(rdn(rdnn(n6),rdnn(n6)))),
inference(clausify,[status(thm)],[f_194_1]) ).
fof(f_195_1,plain,
rdn_translate(nn67,rdn_neg(rdn(rdnn(n7),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn67]) ).
cnf(f_195_2,plain,
rdn_translate(nn67,rdn_neg(rdn(rdnn(n7),rdnn(n6)))),
inference(clausify,[status(thm)],[f_195_1]) ).
fof(f_196_1,plain,
rdn_translate(nn68,rdn_neg(rdn(rdnn(n8),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn68]) ).
cnf(f_196_2,plain,
rdn_translate(nn68,rdn_neg(rdn(rdnn(n8),rdnn(n6)))),
inference(clausify,[status(thm)],[f_196_1]) ).
fof(f_197_1,plain,
rdn_translate(nn69,rdn_neg(rdn(rdnn(n9),rdnn(n6)))),
inference(fof_nnf,[status(thm)],[rdnn69]) ).
cnf(f_197_2,plain,
rdn_translate(nn69,rdn_neg(rdn(rdnn(n9),rdnn(n6)))),
inference(clausify,[status(thm)],[f_197_1]) ).
fof(f_198_1,plain,
rdn_translate(nn70,rdn_neg(rdn(rdnn(n0),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn70]) ).
cnf(f_198_2,plain,
rdn_translate(nn70,rdn_neg(rdn(rdnn(n0),rdnn(n7)))),
inference(clausify,[status(thm)],[f_198_1]) ).
fof(f_199_1,plain,
rdn_translate(nn71,rdn_neg(rdn(rdnn(n1),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn71]) ).
cnf(f_199_2,plain,
rdn_translate(nn71,rdn_neg(rdn(rdnn(n1),rdnn(n7)))),
inference(clausify,[status(thm)],[f_199_1]) ).
fof(f_200_1,plain,
rdn_translate(nn72,rdn_neg(rdn(rdnn(n2),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn72]) ).
cnf(f_200_2,plain,
rdn_translate(nn72,rdn_neg(rdn(rdnn(n2),rdnn(n7)))),
inference(clausify,[status(thm)],[f_200_1]) ).
fof(f_201_1,plain,
rdn_translate(nn73,rdn_neg(rdn(rdnn(n3),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn73]) ).
cnf(f_201_2,plain,
rdn_translate(nn73,rdn_neg(rdn(rdnn(n3),rdnn(n7)))),
inference(clausify,[status(thm)],[f_201_1]) ).
fof(f_202_1,plain,
rdn_translate(nn74,rdn_neg(rdn(rdnn(n4),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn74]) ).
cnf(f_202_2,plain,
rdn_translate(nn74,rdn_neg(rdn(rdnn(n4),rdnn(n7)))),
inference(clausify,[status(thm)],[f_202_1]) ).
fof(f_203_1,plain,
rdn_translate(nn75,rdn_neg(rdn(rdnn(n5),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn75]) ).
cnf(f_203_2,plain,
rdn_translate(nn75,rdn_neg(rdn(rdnn(n5),rdnn(n7)))),
inference(clausify,[status(thm)],[f_203_1]) ).
fof(f_204_1,plain,
rdn_translate(nn76,rdn_neg(rdn(rdnn(n6),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn76]) ).
cnf(f_204_2,plain,
rdn_translate(nn76,rdn_neg(rdn(rdnn(n6),rdnn(n7)))),
inference(clausify,[status(thm)],[f_204_1]) ).
fof(f_205_1,plain,
rdn_translate(nn77,rdn_neg(rdn(rdnn(n7),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn77]) ).
cnf(f_205_2,plain,
rdn_translate(nn77,rdn_neg(rdn(rdnn(n7),rdnn(n7)))),
inference(clausify,[status(thm)],[f_205_1]) ).
fof(f_206_1,plain,
rdn_translate(nn78,rdn_neg(rdn(rdnn(n8),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn78]) ).
cnf(f_206_2,plain,
rdn_translate(nn78,rdn_neg(rdn(rdnn(n8),rdnn(n7)))),
inference(clausify,[status(thm)],[f_206_1]) ).
fof(f_207_1,plain,
rdn_translate(nn79,rdn_neg(rdn(rdnn(n9),rdnn(n7)))),
inference(fof_nnf,[status(thm)],[rdnn79]) ).
cnf(f_207_2,plain,
rdn_translate(nn79,rdn_neg(rdn(rdnn(n9),rdnn(n7)))),
inference(clausify,[status(thm)],[f_207_1]) ).
fof(f_208_1,plain,
rdn_translate(nn80,rdn_neg(rdn(rdnn(n0),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn80]) ).
cnf(f_208_2,plain,
rdn_translate(nn80,rdn_neg(rdn(rdnn(n0),rdnn(n8)))),
inference(clausify,[status(thm)],[f_208_1]) ).
fof(f_209_1,plain,
rdn_translate(nn81,rdn_neg(rdn(rdnn(n1),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn81]) ).
cnf(f_209_2,plain,
rdn_translate(nn81,rdn_neg(rdn(rdnn(n1),rdnn(n8)))),
inference(clausify,[status(thm)],[f_209_1]) ).
fof(f_210_1,plain,
rdn_translate(nn82,rdn_neg(rdn(rdnn(n2),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn82]) ).
cnf(f_210_2,plain,
rdn_translate(nn82,rdn_neg(rdn(rdnn(n2),rdnn(n8)))),
inference(clausify,[status(thm)],[f_210_1]) ).
fof(f_211_1,plain,
rdn_translate(nn83,rdn_neg(rdn(rdnn(n3),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn83]) ).
cnf(f_211_2,plain,
rdn_translate(nn83,rdn_neg(rdn(rdnn(n3),rdnn(n8)))),
inference(clausify,[status(thm)],[f_211_1]) ).
fof(f_212_1,plain,
rdn_translate(nn84,rdn_neg(rdn(rdnn(n4),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn84]) ).
cnf(f_212_2,plain,
rdn_translate(nn84,rdn_neg(rdn(rdnn(n4),rdnn(n8)))),
inference(clausify,[status(thm)],[f_212_1]) ).
fof(f_213_1,plain,
rdn_translate(nn85,rdn_neg(rdn(rdnn(n5),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn85]) ).
cnf(f_213_2,plain,
rdn_translate(nn85,rdn_neg(rdn(rdnn(n5),rdnn(n8)))),
inference(clausify,[status(thm)],[f_213_1]) ).
fof(f_214_1,plain,
rdn_translate(nn86,rdn_neg(rdn(rdnn(n6),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn86]) ).
cnf(f_214_2,plain,
rdn_translate(nn86,rdn_neg(rdn(rdnn(n6),rdnn(n8)))),
inference(clausify,[status(thm)],[f_214_1]) ).
fof(f_215_1,plain,
rdn_translate(nn87,rdn_neg(rdn(rdnn(n7),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn87]) ).
cnf(f_215_2,plain,
rdn_translate(nn87,rdn_neg(rdn(rdnn(n7),rdnn(n8)))),
inference(clausify,[status(thm)],[f_215_1]) ).
fof(f_216_1,plain,
rdn_translate(nn88,rdn_neg(rdn(rdnn(n8),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn88]) ).
cnf(f_216_2,plain,
rdn_translate(nn88,rdn_neg(rdn(rdnn(n8),rdnn(n8)))),
inference(clausify,[status(thm)],[f_216_1]) ).
fof(f_217_1,plain,
rdn_translate(nn89,rdn_neg(rdn(rdnn(n9),rdnn(n8)))),
inference(fof_nnf,[status(thm)],[rdnn89]) ).
cnf(f_217_2,plain,
rdn_translate(nn89,rdn_neg(rdn(rdnn(n9),rdnn(n8)))),
inference(clausify,[status(thm)],[f_217_1]) ).
fof(f_218_1,plain,
rdn_translate(nn90,rdn_neg(rdn(rdnn(n0),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn90]) ).
cnf(f_218_2,plain,
rdn_translate(nn90,rdn_neg(rdn(rdnn(n0),rdnn(n9)))),
inference(clausify,[status(thm)],[f_218_1]) ).
fof(f_219_1,plain,
rdn_translate(nn91,rdn_neg(rdn(rdnn(n1),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn91]) ).
cnf(f_219_2,plain,
rdn_translate(nn91,rdn_neg(rdn(rdnn(n1),rdnn(n9)))),
inference(clausify,[status(thm)],[f_219_1]) ).
fof(f_220_1,plain,
rdn_translate(nn92,rdn_neg(rdn(rdnn(n2),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn92]) ).
cnf(f_220_2,plain,
rdn_translate(nn92,rdn_neg(rdn(rdnn(n2),rdnn(n9)))),
inference(clausify,[status(thm)],[f_220_1]) ).
fof(f_221_1,plain,
rdn_translate(nn93,rdn_neg(rdn(rdnn(n3),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn93]) ).
cnf(f_221_2,plain,
rdn_translate(nn93,rdn_neg(rdn(rdnn(n3),rdnn(n9)))),
inference(clausify,[status(thm)],[f_221_1]) ).
fof(f_222_1,plain,
rdn_translate(nn94,rdn_neg(rdn(rdnn(n4),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn94]) ).
cnf(f_222_2,plain,
rdn_translate(nn94,rdn_neg(rdn(rdnn(n4),rdnn(n9)))),
inference(clausify,[status(thm)],[f_222_1]) ).
fof(f_223_1,plain,
rdn_translate(nn95,rdn_neg(rdn(rdnn(n5),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn95]) ).
cnf(f_223_2,plain,
rdn_translate(nn95,rdn_neg(rdn(rdnn(n5),rdnn(n9)))),
inference(clausify,[status(thm)],[f_223_1]) ).
fof(f_224_1,plain,
rdn_translate(nn96,rdn_neg(rdn(rdnn(n6),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn96]) ).
cnf(f_224_2,plain,
rdn_translate(nn96,rdn_neg(rdn(rdnn(n6),rdnn(n9)))),
inference(clausify,[status(thm)],[f_224_1]) ).
fof(f_225_1,plain,
rdn_translate(nn97,rdn_neg(rdn(rdnn(n7),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn97]) ).
cnf(f_225_2,plain,
rdn_translate(nn97,rdn_neg(rdn(rdnn(n7),rdnn(n9)))),
inference(clausify,[status(thm)],[f_225_1]) ).
fof(f_226_1,plain,
rdn_translate(nn98,rdn_neg(rdn(rdnn(n8),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn98]) ).
cnf(f_226_2,plain,
rdn_translate(nn98,rdn_neg(rdn(rdnn(n8),rdnn(n9)))),
inference(clausify,[status(thm)],[f_226_1]) ).
fof(f_227_1,plain,
rdn_translate(nn99,rdn_neg(rdn(rdnn(n9),rdnn(n9)))),
inference(fof_nnf,[status(thm)],[rdnn99]) ).
cnf(f_227_2,plain,
rdn_translate(nn99,rdn_neg(rdn(rdnn(n9),rdnn(n9)))),
inference(clausify,[status(thm)],[f_227_1]) ).
fof(f_228_1,plain,
rdn_translate(nn100,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn100]) ).
cnf(f_228_2,plain,
rdn_translate(nn100,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_228_1]) ).
fof(f_229_1,plain,
rdn_translate(nn101,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn101]) ).
cnf(f_229_2,plain,
rdn_translate(nn101,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_229_1]) ).
fof(f_230_1,plain,
rdn_translate(nn102,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn102]) ).
cnf(f_230_2,plain,
rdn_translate(nn102,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_230_1]) ).
fof(f_231_1,plain,
rdn_translate(nn103,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn103]) ).
cnf(f_231_2,plain,
rdn_translate(nn103,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_231_1]) ).
fof(f_232_1,plain,
rdn_translate(nn104,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn104]) ).
cnf(f_232_2,plain,
rdn_translate(nn104,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_232_1]) ).
fof(f_233_1,plain,
rdn_translate(nn105,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn105]) ).
cnf(f_233_2,plain,
rdn_translate(nn105,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_233_1]) ).
fof(f_234_1,plain,
rdn_translate(nn106,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn106]) ).
cnf(f_234_2,plain,
rdn_translate(nn106,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_234_1]) ).
fof(f_235_1,plain,
rdn_translate(nn107,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn107]) ).
cnf(f_235_2,plain,
rdn_translate(nn107,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_235_1]) ).
fof(f_236_1,plain,
rdn_translate(nn108,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn108]) ).
cnf(f_236_2,plain,
rdn_translate(nn108,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_236_1]) ).
fof(f_237_1,plain,
rdn_translate(nn109,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn109]) ).
cnf(f_237_2,plain,
rdn_translate(nn109,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n0),rdnn(n1))))),
inference(clausify,[status(thm)],[f_237_1]) ).
fof(f_238_1,plain,
rdn_translate(nn110,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn110]) ).
cnf(f_238_2,plain,
rdn_translate(nn110,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_238_1]) ).
fof(f_239_1,plain,
rdn_translate(nn111,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn111]) ).
cnf(f_239_2,plain,
rdn_translate(nn111,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_239_1]) ).
fof(f_240_1,plain,
rdn_translate(nn112,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn112]) ).
cnf(f_240_2,plain,
rdn_translate(nn112,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_240_1]) ).
fof(f_241_1,plain,
rdn_translate(nn113,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn113]) ).
cnf(f_241_2,plain,
rdn_translate(nn113,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_241_1]) ).
fof(f_242_1,plain,
rdn_translate(nn114,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn114]) ).
cnf(f_242_2,plain,
rdn_translate(nn114,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_242_1]) ).
fof(f_243_1,plain,
rdn_translate(nn115,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn115]) ).
cnf(f_243_2,plain,
rdn_translate(nn115,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_243_1]) ).
fof(f_244_1,plain,
rdn_translate(nn116,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn116]) ).
cnf(f_244_2,plain,
rdn_translate(nn116,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_244_1]) ).
fof(f_245_1,plain,
rdn_translate(nn117,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn117]) ).
cnf(f_245_2,plain,
rdn_translate(nn117,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_245_1]) ).
fof(f_246_1,plain,
rdn_translate(nn118,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn118]) ).
cnf(f_246_2,plain,
rdn_translate(nn118,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_246_1]) ).
fof(f_247_1,plain,
rdn_translate(nn119,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn119]) ).
cnf(f_247_2,plain,
rdn_translate(nn119,rdn_neg(rdn(rdnn(n9),rdn(rdnn(n1),rdnn(n1))))),
inference(clausify,[status(thm)],[f_247_1]) ).
fof(f_248_1,plain,
rdn_translate(nn120,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn120]) ).
cnf(f_248_2,plain,
rdn_translate(nn120,rdn_neg(rdn(rdnn(n0),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_248_1]) ).
fof(f_249_1,plain,
rdn_translate(nn121,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn121]) ).
cnf(f_249_2,plain,
rdn_translate(nn121,rdn_neg(rdn(rdnn(n1),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_249_1]) ).
fof(f_250_1,plain,
rdn_translate(nn122,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn122]) ).
cnf(f_250_2,plain,
rdn_translate(nn122,rdn_neg(rdn(rdnn(n2),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_250_1]) ).
fof(f_251_1,plain,
rdn_translate(nn123,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn123]) ).
cnf(f_251_2,plain,
rdn_translate(nn123,rdn_neg(rdn(rdnn(n3),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_251_1]) ).
fof(f_252_1,plain,
rdn_translate(nn124,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn124]) ).
cnf(f_252_2,plain,
rdn_translate(nn124,rdn_neg(rdn(rdnn(n4),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_252_1]) ).
fof(f_253_1,plain,
rdn_translate(nn125,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn125]) ).
cnf(f_253_2,plain,
rdn_translate(nn125,rdn_neg(rdn(rdnn(n5),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_253_1]) ).
fof(f_254_1,plain,
rdn_translate(nn126,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn126]) ).
cnf(f_254_2,plain,
rdn_translate(nn126,rdn_neg(rdn(rdnn(n6),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_254_1]) ).
fof(f_255_1,plain,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn127]) ).
cnf(f_255_2,plain,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_255_1]) ).
fof(f_256_1,plain,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
inference(fof_nnf,[status(thm)],[rdnn128]) ).
cnf(f_256_2,plain,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
inference(clausify,[status(thm)],[f_256_1]) ).
fof(f_257_1,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit1]) ).
cnf(f_257_2,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(clausify,[status(thm)],[f_257_1]) ).
fof(f_258_1,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(fof_nnf,[status(thm)],[rdn_digit2]) ).
cnf(f_258_2,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(clausify,[status(thm)],[f_258_1]) ).
fof(f_259_1,plain,
rdn_non_zero_digit(rdnn(n3)),
inference(fof_nnf,[status(thm)],[rdn_digit3]) ).
cnf(f_259_2,plain,
rdn_non_zero_digit(rdnn(n3)),
inference(clausify,[status(thm)],[f_259_1]) ).
fof(f_260_1,plain,
rdn_non_zero_digit(rdnn(n4)),
inference(fof_nnf,[status(thm)],[rdn_digit4]) ).
cnf(f_260_2,plain,
rdn_non_zero_digit(rdnn(n4)),
inference(clausify,[status(thm)],[f_260_1]) ).
fof(f_261_1,plain,
rdn_non_zero_digit(rdnn(n5)),
inference(fof_nnf,[status(thm)],[rdn_digit5]) ).
cnf(f_261_2,plain,
rdn_non_zero_digit(rdnn(n5)),
inference(clausify,[status(thm)],[f_261_1]) ).
fof(f_262_1,plain,
rdn_non_zero_digit(rdnn(n6)),
inference(fof_nnf,[status(thm)],[rdn_digit6]) ).
cnf(f_262_2,plain,
rdn_non_zero_digit(rdnn(n6)),
inference(clausify,[status(thm)],[f_262_1]) ).
fof(f_263_1,plain,
rdn_non_zero_digit(rdnn(n7)),
inference(fof_nnf,[status(thm)],[rdn_digit7]) ).
cnf(f_263_2,plain,
rdn_non_zero_digit(rdnn(n7)),
inference(clausify,[status(thm)],[f_263_1]) ).
fof(f_264_1,plain,
rdn_non_zero_digit(rdnn(n8)),
inference(fof_nnf,[status(thm)],[rdn_digit8]) ).
cnf(f_264_2,plain,
rdn_non_zero_digit(rdnn(n8)),
inference(clausify,[status(thm)],[f_264_1]) ).
fof(f_265_1,plain,
rdn_non_zero_digit(rdnn(n9)),
inference(fof_nnf,[status(thm)],[rdn_digit9]) ).
cnf(f_265_2,plain,
rdn_non_zero_digit(rdnn(n9)),
inference(clausify,[status(thm)],[f_265_1]) ).
fof(f_266_1,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_positive_less01]) ).
cnf(f_266_2,plain,
rdn_positive_less(rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_266_1]) ).
fof(f_267_1,plain,
rdn_positive_less(rdnn(n1),rdnn(n2)),
inference(fof_nnf,[status(thm)],[rdn_positive_less12]) ).
cnf(f_267_2,plain,
rdn_positive_less(rdnn(n1),rdnn(n2)),
inference(clausify,[status(thm)],[f_267_1]) ).
fof(f_268_1,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(fof_nnf,[status(thm)],[rdn_positive_less23]) ).
cnf(f_268_2,plain,
rdn_positive_less(rdnn(n2),rdnn(n3)),
inference(clausify,[status(thm)],[f_268_1]) ).
fof(f_269_1,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(fof_nnf,[status(thm)],[rdn_positive_less34]) ).
cnf(f_269_2,plain,
rdn_positive_less(rdnn(n3),rdnn(n4)),
inference(clausify,[status(thm)],[f_269_1]) ).
fof(f_270_1,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(fof_nnf,[status(thm)],[rdn_positive_less45]) ).
cnf(f_270_2,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(clausify,[status(thm)],[f_270_1]) ).
fof(f_271_1,plain,
rdn_positive_less(rdnn(n5),rdnn(n6)),
inference(fof_nnf,[status(thm)],[rdn_positive_less56]) ).
cnf(f_271_2,plain,
rdn_positive_less(rdnn(n5),rdnn(n6)),
inference(clausify,[status(thm)],[f_271_1]) ).
fof(f_272_1,plain,
rdn_positive_less(rdnn(n6),rdnn(n7)),
inference(fof_nnf,[status(thm)],[rdn_positive_less67]) ).
cnf(f_272_2,plain,
rdn_positive_less(rdnn(n6),rdnn(n7)),
inference(clausify,[status(thm)],[f_272_1]) ).
fof(f_273_1,plain,
rdn_positive_less(rdnn(n7),rdnn(n8)),
inference(fof_nnf,[status(thm)],[rdn_positive_less78]) ).
cnf(f_273_2,plain,
rdn_positive_less(rdnn(n7),rdnn(n8)),
inference(clausify,[status(thm)],[f_273_1]) ).
fof(f_274_1,plain,
rdn_positive_less(rdnn(n8),rdnn(n9)),
inference(fof_nnf,[status(thm)],[rdn_positive_less89]) ).
cnf(f_274_2,plain,
rdn_positive_less(rdnn(n8),rdnn(n9)),
inference(clausify,[status(thm)],[f_274_1]) ).
fof(f_275_1,plain,
! [X,Y,Z] :
( rdn_positive_less(rdnn(X),rdnn(Z))
| ~ rdn_positive_less(rdnn(Y),rdnn(Z))
| ~ rdn_positive_less(rdnn(X),rdnn(Y)) ),
inference(fof_nnf,[status(thm)],[rdn_positive_less_transitivity]) ).
fof(f_275_2,plain,
! [U_2,U_1,U_0] :
( rdn_positive_less(rdnn(U_2),rdnn(U_0))
| ~ rdn_positive_less(rdnn(U_1),rdnn(U_0))
| ~ rdn_positive_less(rdnn(U_2),rdnn(U_1)) ),
inference(variable_rename,[status(thm)],[f_275_1]) ).
cnf(f_275_3,plain,
( rdn_positive_less(rdnn(U_2),rdnn(U_0))
| ~ rdn_positive_less(rdnn(U_1),rdnn(U_0))
| ~ rdn_positive_less(rdnn(U_2),rdnn(U_1)) ),
inference(clausify,[status(thm)],[f_275_2]) ).
fof(f_276_1,plain,
! [Ds,Os,Db,Ob] :
( rdn_positive_less(rdn(rdnn(Ds),Os),rdn(rdnn(Db),Ob))
| ~ rdn_positive_less(Os,Ob) ),
inference(fof_nnf,[status(thm)],[rdn_positive_less_multi_digit_high]) ).
fof(f_276_2,plain,
! [U_6,U_5,U_4,U_3] :
( rdn_positive_less(rdn(rdnn(U_6),U_5),rdn(rdnn(U_4),U_3))
| ~ rdn_positive_less(U_5,U_3) ),
inference(variable_rename,[status(thm)],[f_276_1]) ).
cnf(f_276_3,plain,
( rdn_positive_less(rdn(rdnn(U_6),U_5),rdn(rdnn(U_4),U_3))
| ~ rdn_positive_less(U_5,U_3) ),
inference(clausify,[status(thm)],[f_276_2]) ).
fof(f_277_1,plain,
! [Ds,O,Db] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_non_zero(O)
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db)) ),
inference(fof_nnf,[status(thm)],[rdn_positive_less_multi_digit_low]) ).
fof(f_277_2,plain,
! [U_9,U_8,U_7] :
( rdn_positive_less(rdn(rdnn(U_9),U_8),rdn(rdnn(U_7),U_8))
| ~ rdn_non_zero(U_8)
| ~ rdn_positive_less(rdnn(U_9),rdnn(U_7)) ),
inference(variable_rename,[status(thm)],[f_277_1]) ).
cnf(f_277_3,plain,
( rdn_positive_less(rdn(rdnn(U_9),U_8),rdn(rdnn(U_7),U_8))
| ~ rdn_non_zero(U_8)
| ~ rdn_positive_less(rdnn(U_9),rdnn(U_7)) ),
inference(clausify,[status(thm)],[f_277_2]) ).
fof(f_278_1,plain,
! [D,Db,Ob] :
( rdn_positive_less(rdnn(D),rdn(rdnn(Db),Ob))
| ~ rdn_non_zero(Ob) ),
inference(fof_nnf,[status(thm)],[rdn_extra_digits_positive_less]) ).
fof(f_278_2,plain,
! [U_12,U_11,U_10] :
( rdn_positive_less(rdnn(U_12),rdn(rdnn(U_11),U_10))
| ~ rdn_non_zero(U_10) ),
inference(variable_rename,[status(thm)],[f_278_1]) ).
cnf(f_278_3,plain,
( rdn_positive_less(rdnn(U_12),rdn(rdnn(U_11),U_10))
| ~ rdn_non_zero(U_10) ),
inference(clausify,[status(thm)],[f_278_2]) ).
fof(f_279_1,plain,
! [X] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(fof_nnf,[status(thm)],[rdn_non_zero_by_digit]) ).
fof(f_279_2,plain,
! [U_13] :
( rdn_non_zero(rdnn(U_13))
| ~ rdn_non_zero_digit(rdnn(U_13)) ),
inference(variable_rename,[status(thm)],[f_279_1]) ).
cnf(f_279_3,plain,
( rdn_non_zero(rdnn(U_13))
| ~ rdn_non_zero_digit(rdnn(U_13)) ),
inference(clausify,[status(thm)],[f_279_2]) ).
fof(f_280_1,plain,
! [D,O] :
( rdn_non_zero(rdn(rdnn(D),O))
| ~ rdn_non_zero(O) ),
inference(fof_nnf,[status(thm)],[rdn_non_zero_by_structure]) ).
fof(f_280_2,plain,
! [U_15,U_14] :
( rdn_non_zero(rdn(rdnn(U_15),U_14))
| ~ rdn_non_zero(U_14) ),
inference(variable_rename,[status(thm)],[f_280_1]) ).
cnf(f_280_3,plain,
( rdn_non_zero(rdn(rdnn(U_15),U_14))
| ~ rdn_non_zero(U_14) ),
inference(clausify,[status(thm)],[f_280_2]) ).
fof(f_281_1,plain,
! [X,Y,RDN_X,RDN_Y] :
( less(X,Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(fof_nnf,[status(thm)],[less_entry_point_pos_pos]) ).
fof(f_281_2,plain,
! [U_19,U_18,U_17,U_16] :
( less(U_19,U_18)
| ~ rdn_positive_less(U_17,U_16)
| ~ rdn_translate(U_18,rdn_pos(U_16))
| ~ rdn_translate(U_19,rdn_pos(U_17)) ),
inference(variable_rename,[status(thm)],[f_281_1]) ).
fof(f_281_3,plain,
! [U_19,U_18] :
( ! [U_17] :
( ! [U_16] :
( ~ rdn_positive_less(U_17,U_16)
| ~ rdn_translate(U_18,rdn_pos(U_16)) )
| ~ rdn_translate(U_19,rdn_pos(U_17)) )
| less(U_19,U_18) ),
inference(miniscope,[status(thm)],[f_281_2]) ).
cnf(f_281_4,plain,
( ~ rdn_positive_less(U_17,U_16)
| ~ rdn_translate(U_18,rdn_pos(U_16))
| ~ rdn_translate(U_19,rdn_pos(U_17))
| less(U_19,U_18) ),
inference(clausify,[status(thm)],[f_281_3]) ).
fof(f_282_1,plain,
! [X,Y,RDN_X,RDN_Y] :
( less(X,Y)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_neg(RDN_X)) ),
inference(fof_nnf,[status(thm)],[less_entry_point_neg_pos]) ).
fof(f_282_2,plain,
! [U_23,U_22,U_21,U_20] :
( less(U_23,U_22)
| ~ rdn_translate(U_22,rdn_pos(U_20))
| ~ rdn_translate(U_23,rdn_neg(U_21)) ),
inference(variable_rename,[status(thm)],[f_282_1]) ).
fof(f_282_3,plain,
! [U_23,U_22] :
( ! [U_21] : ~ rdn_translate(U_23,rdn_neg(U_21))
| ! [U_20] : ~ rdn_translate(U_22,rdn_pos(U_20))
| less(U_23,U_22) ),
inference(miniscope,[status(thm)],[f_282_2]) ).
cnf(f_282_4,plain,
( ~ rdn_translate(U_23,rdn_neg(U_21))
| ~ rdn_translate(U_22,rdn_pos(U_20))
| less(U_23,U_22) ),
inference(clausify,[status(thm)],[f_282_3]) ).
fof(f_283_1,plain,
! [X,Y,RDN_X,RDN_Y] :
( less(X,Y)
| ~ rdn_positive_less(RDN_Y,RDN_X)
| ~ rdn_translate(Y,rdn_neg(RDN_Y))
| ~ rdn_translate(X,rdn_neg(RDN_X)) ),
inference(fof_nnf,[status(thm)],[less_entry_point_neg_neg]) ).
fof(f_283_2,plain,
! [U_27,U_26,U_25,U_24] :
( less(U_27,U_26)
| ~ rdn_positive_less(U_24,U_25)
| ~ rdn_translate(U_26,rdn_neg(U_24))
| ~ rdn_translate(U_27,rdn_neg(U_25)) ),
inference(variable_rename,[status(thm)],[f_283_1]) ).
fof(f_283_3,plain,
! [U_27,U_26] :
( ! [U_25] :
( ! [U_24] :
( ~ rdn_positive_less(U_24,U_25)
| ~ rdn_translate(U_26,rdn_neg(U_24)) )
| ~ rdn_translate(U_27,rdn_neg(U_25)) )
| less(U_27,U_26) ),
inference(miniscope,[status(thm)],[f_283_2]) ).
cnf(f_283_4,plain,
( ~ rdn_positive_less(U_24,U_25)
| ~ rdn_translate(U_26,rdn_neg(U_24))
| ~ rdn_translate(U_27,rdn_neg(U_25))
| less(U_27,U_26) ),
inference(clausify,[status(thm)],[f_283_3]) ).
fof(f_284_1,plain,
! [X,Y] :
( ( less(X,Y)
| Y = X
| less(Y,X) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(fof_nnf,[status(thm)],[less_property]) ).
fof(f_284_2,plain,
! [U_29,U_28] :
( ( less(U_29,U_28)
| U_28 = U_29
| less(U_28,U_29) )
& ( ( U_28 != U_29
& ~ less(U_28,U_29) )
| ~ less(U_29,U_28) ) ),
inference(variable_rename,[status(thm)],[f_284_1]) ).
fof(f_284_3,plain,
( ! [U_33,U_31] :
( less(U_33,U_31)
| U_31 = U_33
| less(U_31,U_33) )
& ! [U_32,U_30] :
( ( U_30 != U_32
& ~ less(U_30,U_32) )
| ~ less(U_32,U_30) ) ),
inference(miniscope,[status(thm)],[f_284_2]) ).
cnf(f_284_4,plain,
( ~ less(U_30,U_32)
| ~ less(U_32,U_30) ),
inference(clausify,[status(thm)],[f_284_3]) ).
cnf(f_284_5,plain,
( U_30 != U_32
| ~ less(U_32,U_30) ),
inference(clausify,[status(thm)],[f_284_3]) ).
cnf(f_284_6,plain,
( less(U_33,U_31)
| U_31 = U_33
| less(U_31,U_33) ),
inference(clausify,[status(thm)],[f_284_3]) ).
fof(f_285_1,plain,
! [X,Y] :
( ( less_or_equal(X,Y)
| ( X != Y
& ~ less(X,Y) ) )
& ( X = Y
| less(X,Y)
| ~ less_or_equal(X,Y) ) ),
inference(fof_nnf,[status(thm)],[less_or_equal]) ).
fof(f_285_2,plain,
! [U_35,U_34] :
( ( less_or_equal(U_35,U_34)
| ( U_35 != U_34
& ~ less(U_35,U_34) ) )
& ( U_35 = U_34
| less(U_35,U_34)
| ~ less_or_equal(U_35,U_34) ) ),
inference(variable_rename,[status(thm)],[f_285_1]) ).
fof(f_285_3,plain,
( ! [U_39,U_37] :
( less_or_equal(U_39,U_37)
| ( U_39 != U_37
& ~ less(U_39,U_37) ) )
& ! [U_38,U_36] :
( U_38 = U_36
| less(U_38,U_36)
| ~ less_or_equal(U_38,U_36) ) ),
inference(miniscope,[status(thm)],[f_285_2]) ).
cnf(f_285_4,plain,
( U_38 = U_36
| less(U_38,U_36)
| ~ less_or_equal(U_38,U_36) ),
inference(clausify,[status(thm)],[f_285_3]) ).
cnf(f_285_5,plain,
( ~ less(U_39,U_37)
| less_or_equal(U_39,U_37) ),
inference(clausify,[status(thm)],[f_285_3]) ).
cnf(f_285_6,plain,
( U_39 != U_37
| less_or_equal(U_39,U_37) ),
inference(clausify,[status(thm)],[f_285_3]) ).
fof(f_286_1,plain,
! [X,Y,Z] :
( less_or_equal(Z,X)
| ~ less(Z,Y)
| ~ sum(X,n1,Y) ),
inference(fof_nnf,[status(thm)],[less_successor]) ).
fof(f_286_2,plain,
! [U_42,U_41,U_40] :
( less_or_equal(U_40,U_42)
| ~ less(U_40,U_41)
| ~ sum(U_42,n1,U_41) ),
inference(variable_rename,[status(thm)],[f_286_1]) ).
cnf(f_286_3,plain,
( less_or_equal(U_40,U_42)
| ~ less(U_40,U_41)
| ~ sum(U_42,n1,U_41) ),
inference(clausify,[status(thm)],[f_286_2]) ).
fof(f_287_1,plain,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( sum(X,Y,Z)
| ~ rdn_translate(Z,rdn_pos(RDN_Z))
| ~ rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Y,RDN_Z)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(fof_nnf,[status(thm)],[sum_entry_point_pos_pos]) ).
fof(f_287_2,plain,
! [U_48,U_47,U_46,U_45,U_44,U_43] :
( sum(U_48,U_47,U_46)
| ~ rdn_translate(U_46,rdn_pos(U_43))
| ~ rdn_add_with_carry(rdnn(n0),U_45,U_44,U_43)
| ~ rdn_translate(U_47,rdn_pos(U_44))
| ~ rdn_translate(U_48,rdn_pos(U_45)) ),
inference(variable_rename,[status(thm)],[f_287_1]) ).
fof(f_287_3,plain,
! [U_48,U_47,U_46] :
( ! [U_45] :
( ! [U_44] :
( ! [U_43] :
( ~ rdn_translate(U_46,rdn_pos(U_43))
| ~ rdn_add_with_carry(rdnn(n0),U_45,U_44,U_43) )
| ~ rdn_translate(U_47,rdn_pos(U_44)) )
| ~ rdn_translate(U_48,rdn_pos(U_45)) )
| sum(U_48,U_47,U_46) ),
inference(miniscope,[status(thm)],[f_287_2]) ).
cnf(f_287_4,plain,
( ~ rdn_translate(U_46,rdn_pos(U_43))
| ~ rdn_add_with_carry(rdnn(n0),U_45,U_44,U_43)
| ~ rdn_translate(U_47,rdn_pos(U_44))
| ~ rdn_translate(U_48,rdn_pos(U_45))
| sum(U_48,U_47,U_46) ),
inference(clausify,[status(thm)],[f_287_3]) ).
fof(f_288_1,plain,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( sum(X,Y,Z)
| ~ rdn_translate(Z,rdn_neg(RDN_Z))
| ~ rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Y,RDN_Z)
| ~ rdn_translate(Y,rdn_neg(RDN_Y))
| ~ rdn_translate(X,rdn_neg(RDN_X)) ),
inference(fof_nnf,[status(thm)],[sum_entry_point_neg_neg]) ).
fof(f_288_2,plain,
! [U_54,U_53,U_52,U_51,U_50,U_49] :
( sum(U_54,U_53,U_52)
| ~ rdn_translate(U_52,rdn_neg(U_49))
| ~ rdn_add_with_carry(rdnn(n0),U_51,U_50,U_49)
| ~ rdn_translate(U_53,rdn_neg(U_50))
| ~ rdn_translate(U_54,rdn_neg(U_51)) ),
inference(variable_rename,[status(thm)],[f_288_1]) ).
fof(f_288_3,plain,
! [U_54,U_53,U_52] :
( ! [U_51] :
( ! [U_50] :
( ! [U_49] :
( ~ rdn_translate(U_52,rdn_neg(U_49))
| ~ rdn_add_with_carry(rdnn(n0),U_51,U_50,U_49) )
| ~ rdn_translate(U_53,rdn_neg(U_50)) )
| ~ rdn_translate(U_54,rdn_neg(U_51)) )
| sum(U_54,U_53,U_52) ),
inference(miniscope,[status(thm)],[f_288_2]) ).
cnf(f_288_4,plain,
( ~ rdn_translate(U_52,rdn_neg(U_49))
| ~ rdn_add_with_carry(rdnn(n0),U_51,U_50,U_49)
| ~ rdn_translate(U_53,rdn_neg(U_50))
| ~ rdn_translate(U_54,rdn_neg(U_51))
| sum(U_54,U_53,U_52) ),
inference(clausify,[status(thm)],[f_288_3]) ).
fof(f_289_1,plain,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( sum(X,Y,Z)
| ~ rdn_translate(Z,rdn_neg(RDN_Z))
| ~ rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Z,RDN_Y)
| ~ rdn_positive_less(RDN_X,RDN_Y)
| ~ rdn_translate(Y,rdn_neg(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(fof_nnf,[status(thm)],[sum_entry_point_pos_neg_1]) ).
fof(f_289_2,plain,
! [U_60,U_59,U_58,U_57,U_56,U_55] :
( sum(U_60,U_59,U_58)
| ~ rdn_translate(U_58,rdn_neg(U_55))
| ~ rdn_add_with_carry(rdnn(n0),U_57,U_55,U_56)
| ~ rdn_positive_less(U_57,U_56)
| ~ rdn_translate(U_59,rdn_neg(U_56))
| ~ rdn_translate(U_60,rdn_pos(U_57)) ),
inference(variable_rename,[status(thm)],[f_289_1]) ).
fof(f_289_3,plain,
! [U_60,U_59,U_58] :
( ! [U_57] :
( ! [U_56] :
( ! [U_55] :
( ~ rdn_translate(U_58,rdn_neg(U_55))
| ~ rdn_add_with_carry(rdnn(n0),U_57,U_55,U_56) )
| ~ rdn_positive_less(U_57,U_56)
| ~ rdn_translate(U_59,rdn_neg(U_56)) )
| ~ rdn_translate(U_60,rdn_pos(U_57)) )
| sum(U_60,U_59,U_58) ),
inference(miniscope,[status(thm)],[f_289_2]) ).
cnf(f_289_4,plain,
( ~ rdn_translate(U_58,rdn_neg(U_55))
| ~ rdn_add_with_carry(rdnn(n0),U_57,U_55,U_56)
| ~ rdn_positive_less(U_57,U_56)
| ~ rdn_translate(U_59,rdn_neg(U_56))
| ~ rdn_translate(U_60,rdn_pos(U_57))
| sum(U_60,U_59,U_58) ),
inference(clausify,[status(thm)],[f_289_3]) ).
fof(f_290_1,plain,
! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :
( sum(X,Y,Z)
| ~ rdn_translate(Z,rdn_pos(RDN_Z))
| ~ rdn_add_with_carry(rdnn(n0),RDN_Y,RDN_Z,RDN_X)
| ~ rdn_positive_less(RDN_Y,RDN_X)
| ~ rdn_translate(Y,rdn_neg(RDN_Y))
| ~ rdn_translate(X,rdn_pos(RDN_X)) ),
inference(fof_nnf,[status(thm)],[sum_entry_point_pos_neg_2]) ).
fof(f_290_2,plain,
! [U_66,U_65,U_64,U_63,U_62,U_61] :
( sum(U_66,U_65,U_64)
| ~ rdn_translate(U_64,rdn_pos(U_61))
| ~ rdn_add_with_carry(rdnn(n0),U_62,U_61,U_63)
| ~ rdn_positive_less(U_62,U_63)
| ~ rdn_translate(U_65,rdn_neg(U_62))
| ~ rdn_translate(U_66,rdn_pos(U_63)) ),
inference(variable_rename,[status(thm)],[f_290_1]) ).
fof(f_290_3,plain,
! [U_66,U_65,U_64] :
( ! [U_63] :
( ! [U_62] :
( ! [U_61] :
( ~ rdn_translate(U_64,rdn_pos(U_61))
| ~ rdn_add_with_carry(rdnn(n0),U_62,U_61,U_63) )
| ~ rdn_positive_less(U_62,U_63)
| ~ rdn_translate(U_65,rdn_neg(U_62)) )
| ~ rdn_translate(U_66,rdn_pos(U_63)) )
| sum(U_66,U_65,U_64) ),
inference(miniscope,[status(thm)],[f_290_2]) ).
cnf(f_290_4,plain,
( ~ rdn_translate(U_64,rdn_pos(U_61))
| ~ rdn_add_with_carry(rdnn(n0),U_62,U_61,U_63)
| ~ rdn_positive_less(U_62,U_63)
| ~ rdn_translate(U_65,rdn_neg(U_62))
| ~ rdn_translate(U_66,rdn_pos(U_63))
| sum(U_66,U_65,U_64) ),
inference(clausify,[status(thm)],[f_290_3]) ).
fof(f_291_1,plain,
! [POS_X,NEG_X,RDN_X] :
( sum(POS_X,NEG_X,n0)
| ~ rdn_translate(NEG_X,rdn_neg(RDN_X))
| ~ rdn_translate(POS_X,rdn_pos(RDN_X)) ),
inference(fof_nnf,[status(thm)],[sum_entry_point_posx_negx]) ).
fof(f_291_2,plain,
! [U_69,U_68,U_67] :
( sum(U_69,U_68,n0)
| ~ rdn_translate(U_68,rdn_neg(U_67))
| ~ rdn_translate(U_69,rdn_pos(U_67)) ),
inference(variable_rename,[status(thm)],[f_291_1]) ).
fof(f_291_3,plain,
! [U_69,U_68] :
( ! [U_67] :
( ~ rdn_translate(U_68,rdn_neg(U_67))
| ~ rdn_translate(U_69,rdn_pos(U_67)) )
| sum(U_69,U_68,n0) ),
inference(miniscope,[status(thm)],[f_291_2]) ).
cnf(f_291_4,plain,
( ~ rdn_translate(U_68,rdn_neg(U_67))
| ~ rdn_translate(U_69,rdn_pos(U_67))
| sum(U_69,U_68,n0) ),
inference(clausify,[status(thm)],[f_291_3]) ).
fof(f_292_1,plain,
! [X,Y,Z,RDN_X,RDN_Y] :
( sum(X,Y,Z)
| ~ sum(Y,X,Z)
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_translate(X,rdn_neg(RDN_X)) ),
inference(fof_nnf,[status(thm)],[sum_entry_point_neg_pos]) ).
fof(f_292_2,plain,
! [U_74,U_73,U_72,U_71,U_70] :
( sum(U_74,U_73,U_72)
| ~ sum(U_73,U_74,U_72)
| ~ rdn_translate(U_73,rdn_pos(U_70))
| ~ rdn_translate(U_74,rdn_neg(U_71)) ),
inference(variable_rename,[status(thm)],[f_292_1]) ).
fof(f_292_3,plain,
! [U_74,U_73,U_72] :
( ! [U_71] : ~ rdn_translate(U_74,rdn_neg(U_71))
| ! [U_70] : ~ rdn_translate(U_73,rdn_pos(U_70))
| ~ sum(U_73,U_74,U_72)
| sum(U_74,U_73,U_72) ),
inference(miniscope,[status(thm)],[f_292_2]) ).
cnf(f_292_4,plain,
( ~ rdn_translate(U_74,rdn_neg(U_71))
| ~ rdn_translate(U_73,rdn_pos(U_70))
| ~ sum(U_73,U_74,U_72)
| sum(U_74,U_73,U_72) ),
inference(clausify,[status(thm)],[f_292_3]) ).
fof(f_293_1,plain,
! [X,Y,Z1,Z2] :
( Z1 = Z2
| ~ sum(X,Y,Z2)
| ~ sum(X,Y,Z1) ),
inference(fof_nnf,[status(thm)],[unique_sum]) ).
fof(f_293_2,plain,
! [U_78,U_77,U_76,U_75] :
( U_76 = U_75
| ~ sum(U_78,U_77,U_75)
| ~ sum(U_78,U_77,U_76) ),
inference(variable_rename,[status(thm)],[f_293_1]) ).
cnf(f_293_3,plain,
( U_76 = U_75
| ~ sum(U_78,U_77,U_75)
| ~ sum(U_78,U_77,U_76) ),
inference(clausify,[status(thm)],[f_293_2]) ).
fof(f_294_1,plain,
! [X1,X2,Y,Z] :
( X1 = X2
| ~ sum(X2,Y,Z)
| ~ sum(X1,Y,Z) ),
inference(fof_nnf,[status(thm)],[unique_LHS]) ).
fof(f_294_2,plain,
! [U_82,U_81,U_80,U_79] :
( U_82 = U_81
| ~ sum(U_81,U_80,U_79)
| ~ sum(U_82,U_80,U_79) ),
inference(variable_rename,[status(thm)],[f_294_1]) ).
fof(f_294_3,plain,
! [U_82,U_81] :
( ! [U_80,U_79] :
( ~ sum(U_81,U_80,U_79)
| ~ sum(U_82,U_80,U_79) )
| U_82 = U_81 ),
inference(miniscope,[status(thm)],[f_294_2]) ).
cnf(f_294_4,plain,
( ~ sum(U_81,U_80,U_79)
| ~ sum(U_82,U_80,U_79)
| U_82 = U_81 ),
inference(clausify,[status(thm)],[f_294_3]) ).
fof(f_295_1,plain,
! [X,Y1,Y2,Z] :
( Y1 = Y2
| ~ sum(X,Y2,Z)
| ~ sum(X,Y1,Z) ),
inference(fof_nnf,[status(thm)],[unique_RHS]) ).
fof(f_295_2,plain,
! [U_86,U_85,U_84,U_83] :
( U_85 = U_84
| ~ sum(U_86,U_84,U_83)
| ~ sum(U_86,U_85,U_83) ),
inference(variable_rename,[status(thm)],[f_295_1]) ).
fof(f_295_3,plain,
! [U_86,U_85,U_84] :
( ! [U_83] :
( ~ sum(U_86,U_84,U_83)
| ~ sum(U_86,U_85,U_83) )
| U_85 = U_84 ),
inference(miniscope,[status(thm)],[f_295_2]) ).
cnf(f_295_4,plain,
( ~ sum(U_86,U_84,U_83)
| ~ sum(U_86,U_85,U_83)
| U_85 = U_84 ),
inference(clausify,[status(thm)],[f_295_3]) ).
fof(f_296_1,plain,
! [X,Y,Z] :
( ( sum(Y,Z,X)
| ~ difference(X,Y,Z) )
& ( difference(X,Y,Z)
| ~ sum(Y,Z,X) ) ),
inference(fof_nnf,[status(thm)],[minus_entry_point]) ).
fof(f_296_2,plain,
! [U_89,U_88,U_87] :
( ( sum(U_88,U_87,U_89)
| ~ difference(U_89,U_88,U_87) )
& ( difference(U_89,U_88,U_87)
| ~ sum(U_88,U_87,U_89) ) ),
inference(variable_rename,[status(thm)],[f_296_1]) ).
fof(f_296_3,plain,
( ! [U_95,U_93,U_91] :
( sum(U_93,U_91,U_95)
| ~ difference(U_95,U_93,U_91) )
& ! [U_94,U_92,U_90] :
( difference(U_94,U_92,U_90)
| ~ sum(U_92,U_90,U_94) ) ),
inference(miniscope,[status(thm)],[f_296_2]) ).
cnf(f_296_4,plain,
( difference(U_94,U_92,U_90)
| ~ sum(U_92,U_90,U_94) ),
inference(clausify,[status(thm)],[f_296_3]) ).
cnf(f_296_5,plain,
( sum(U_93,U_91,U_95)
| ~ difference(U_95,U_93,U_91) ),
inference(clausify,[status(thm)],[f_296_3]) ).
fof(f_297_1,plain,
! [C,D1,D2,RD,ID] :
( rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdnn(RD))
| ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(n0))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(n0)) ),
inference(fof_nnf,[status(thm)],[add_digit_digit_digit]) ).
fof(f_297_2,plain,
! [U_100,U_99,U_98,U_97,U_96] :
( rdn_add_with_carry(rdnn(U_100),rdnn(U_99),rdnn(U_98),rdnn(U_97))
| ~ rdn_digit_add(rdnn(U_96),rdnn(U_100),rdnn(U_97),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_99),rdnn(U_98),rdnn(U_96),rdnn(n0)) ),
inference(variable_rename,[status(thm)],[f_297_1]) ).
fof(f_297_3,plain,
! [U_100,U_99,U_98,U_97] :
( ! [U_96] :
( ~ rdn_digit_add(rdnn(U_96),rdnn(U_100),rdnn(U_97),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_99),rdnn(U_98),rdnn(U_96),rdnn(n0)) )
| rdn_add_with_carry(rdnn(U_100),rdnn(U_99),rdnn(U_98),rdnn(U_97)) ),
inference(miniscope,[status(thm)],[f_297_2]) ).
cnf(f_297_4,plain,
( ~ rdn_digit_add(rdnn(U_96),rdnn(U_100),rdnn(U_97),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_99),rdnn(U_98),rdnn(U_96),rdnn(n0))
| rdn_add_with_carry(rdnn(U_100),rdnn(U_99),rdnn(U_98),rdnn(U_97)) ),
inference(clausify,[status(thm)],[f_297_3]) ).
fof(f_298_1,plain,
! [C,D1,D2,ID,RD,IC1,IC2] :
( rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdn(rdnn(RD),rdnn(n1)))
| ~ rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(n1),rdnn(n0))
| ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) ),
inference(fof_nnf,[status(thm)],[add_digit_digit_rdn]) ).
fof(f_298_2,plain,
! [U_107,U_106,U_105,U_104,U_103,U_102,U_101] :
( rdn_add_with_carry(rdnn(U_107),rdnn(U_106),rdnn(U_105),rdn(rdnn(U_103),rdnn(n1)))
| ~ rdn_digit_add(rdnn(U_102),rdnn(U_101),rdnn(n1),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_104),rdnn(U_107),rdnn(U_103),rdnn(U_101))
| ~ rdn_digit_add(rdnn(U_106),rdnn(U_105),rdnn(U_104),rdnn(U_102)) ),
inference(variable_rename,[status(thm)],[f_298_1]) ).
fof(f_298_3,plain,
! [U_107,U_106,U_105,U_104,U_103] :
( ! [U_102] :
( ! [U_101] :
( ~ rdn_digit_add(rdnn(U_102),rdnn(U_101),rdnn(n1),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_104),rdnn(U_107),rdnn(U_103),rdnn(U_101)) )
| ~ rdn_digit_add(rdnn(U_106),rdnn(U_105),rdnn(U_104),rdnn(U_102)) )
| rdn_add_with_carry(rdnn(U_107),rdnn(U_106),rdnn(U_105),rdn(rdnn(U_103),rdnn(n1))) ),
inference(miniscope,[status(thm)],[f_298_2]) ).
cnf(f_298_4,plain,
( ~ rdn_digit_add(rdnn(U_102),rdnn(U_101),rdnn(n1),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_104),rdnn(U_107),rdnn(U_103),rdnn(U_101))
| ~ rdn_digit_add(rdnn(U_106),rdnn(U_105),rdnn(U_104),rdnn(U_102))
| rdn_add_with_carry(rdnn(U_107),rdnn(U_106),rdnn(U_105),rdn(rdnn(U_103),rdnn(n1))) ),
inference(clausify,[status(thm)],[f_298_3]) ).
fof(f_299_1,plain,
! [C,D1,D2,O2,RD,RO,ID,IC1,IC2,NC] :
( rdn_add_with_carry(rdnn(C),rdnn(D1),rdn(rdnn(D2),O2),rdn(rdnn(RD),RO))
| ~ rdn_non_zero(RO)
| ~ rdn_non_zero(O2)
| ~ rdn_add_with_carry(rdnn(NC),rdnn(n0),O2,RO)
| ~ rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(NC),rdnn(n0))
| ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) ),
inference(fof_nnf,[status(thm)],[add_digit_rdn_rdn]) ).
fof(f_299_2,plain,
! [U_117,U_116,U_115,U_114,U_113,U_112,U_111,U_110,U_109,U_108] :
( rdn_add_with_carry(rdnn(U_117),rdnn(U_116),rdn(rdnn(U_115),U_114),rdn(rdnn(U_113),U_112))
| ~ rdn_non_zero(U_112)
| ~ rdn_non_zero(U_114)
| ~ rdn_add_with_carry(rdnn(U_108),rdnn(n0),U_114,U_112)
| ~ rdn_digit_add(rdnn(U_110),rdnn(U_109),rdnn(U_108),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_111),rdnn(U_117),rdnn(U_113),rdnn(U_109))
| ~ rdn_digit_add(rdnn(U_116),rdnn(U_115),rdnn(U_111),rdnn(U_110)) ),
inference(variable_rename,[status(thm)],[f_299_1]) ).
fof(f_299_3,plain,
! [U_117,U_116,U_115,U_114,U_113,U_112] :
( ! [U_111,U_110] :
( ! [U_109] :
( ! [U_108] :
( ~ rdn_add_with_carry(rdnn(U_108),rdnn(n0),U_114,U_112)
| ~ rdn_digit_add(rdnn(U_110),rdnn(U_109),rdnn(U_108),rdnn(n0)) )
| ~ rdn_digit_add(rdnn(U_111),rdnn(U_117),rdnn(U_113),rdnn(U_109)) )
| ~ rdn_digit_add(rdnn(U_116),rdnn(U_115),rdnn(U_111),rdnn(U_110)) )
| ~ rdn_non_zero(U_112)
| ~ rdn_non_zero(U_114)
| rdn_add_with_carry(rdnn(U_117),rdnn(U_116),rdn(rdnn(U_115),U_114),rdn(rdnn(U_113),U_112)) ),
inference(miniscope,[status(thm)],[f_299_2]) ).
cnf(f_299_4,plain,
( ~ rdn_add_with_carry(rdnn(U_108),rdnn(n0),U_114,U_112)
| ~ rdn_digit_add(rdnn(U_110),rdnn(U_109),rdnn(U_108),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_111),rdnn(U_117),rdnn(U_113),rdnn(U_109))
| ~ rdn_digit_add(rdnn(U_116),rdnn(U_115),rdnn(U_111),rdnn(U_110))
| ~ rdn_non_zero(U_112)
| ~ rdn_non_zero(U_114)
| rdn_add_with_carry(rdnn(U_117),rdnn(U_116),rdn(rdnn(U_115),U_114),rdn(rdnn(U_113),U_112)) ),
inference(clausify,[status(thm)],[f_299_3]) ).
fof(f_300_1,plain,
! [C,D1,O1,D2,O2,RD,RO,ID,IC1,IC2,RC] :
( rdn_add_with_carry(rdnn(C),rdn(rdnn(D1),O1),rdn(rdnn(D2),O2),rdn(rdnn(RD),RO))
| ~ rdn_non_zero(RO)
| ~ rdn_non_zero(O2)
| ~ rdn_non_zero(O1)
| ~ rdn_add_with_carry(rdnn(RC),O1,O2,RO)
| ~ rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(RC),rdnn(n0))
| ~ rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))
| ~ rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1)) ),
inference(fof_nnf,[status(thm)],[add_rdn_rdn_rdn]) ).
fof(f_300_2,plain,
! [U_128,U_127,U_126,U_125,U_124,U_123,U_122,U_121,U_120,U_119,U_118] :
( rdn_add_with_carry(rdnn(U_128),rdn(rdnn(U_127),U_126),rdn(rdnn(U_125),U_124),rdn(rdnn(U_123),U_122))
| ~ rdn_non_zero(U_122)
| ~ rdn_non_zero(U_124)
| ~ rdn_non_zero(U_126)
| ~ rdn_add_with_carry(rdnn(U_118),U_126,U_124,U_122)
| ~ rdn_digit_add(rdnn(U_120),rdnn(U_119),rdnn(U_118),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_121),rdnn(U_128),rdnn(U_123),rdnn(U_119))
| ~ rdn_digit_add(rdnn(U_127),rdnn(U_125),rdnn(U_121),rdnn(U_120)) ),
inference(variable_rename,[status(thm)],[f_300_1]) ).
fof(f_300_3,plain,
! [U_128,U_127,U_126,U_125,U_124,U_123,U_122] :
( ! [U_121,U_120] :
( ! [U_119] :
( ! [U_118] :
( ~ rdn_add_with_carry(rdnn(U_118),U_126,U_124,U_122)
| ~ rdn_digit_add(rdnn(U_120),rdnn(U_119),rdnn(U_118),rdnn(n0)) )
| ~ rdn_digit_add(rdnn(U_121),rdnn(U_128),rdnn(U_123),rdnn(U_119)) )
| ~ rdn_digit_add(rdnn(U_127),rdnn(U_125),rdnn(U_121),rdnn(U_120)) )
| ~ rdn_non_zero(U_122)
| ~ rdn_non_zero(U_124)
| ~ rdn_non_zero(U_126)
| rdn_add_with_carry(rdnn(U_128),rdn(rdnn(U_127),U_126),rdn(rdnn(U_125),U_124),rdn(rdnn(U_123),U_122)) ),
inference(miniscope,[status(thm)],[f_300_2]) ).
cnf(f_300_4,plain,
( ~ rdn_add_with_carry(rdnn(U_118),U_126,U_124,U_122)
| ~ rdn_digit_add(rdnn(U_120),rdnn(U_119),rdnn(U_118),rdnn(n0))
| ~ rdn_digit_add(rdnn(U_121),rdnn(U_128),rdnn(U_123),rdnn(U_119))
| ~ rdn_digit_add(rdnn(U_127),rdnn(U_125),rdnn(U_121),rdnn(U_120))
| ~ rdn_non_zero(U_122)
| ~ rdn_non_zero(U_124)
| ~ rdn_non_zero(U_126)
| rdn_add_with_carry(rdnn(U_128),rdn(rdnn(U_127),U_126),rdn(rdnn(U_125),U_124),rdn(rdnn(U_123),U_122)) ),
inference(clausify,[status(thm)],[f_300_3]) ).
fof(f_301_1,plain,
! [C,D1,O1,D2,RD,RO] :
( rdn_add_with_carry(rdnn(C),rdn(rdnn(D1),O1),rdnn(D2),rdn(rdnn(RD),RO))
| ~ rdn_add_with_carry(rdnn(C),rdnn(D2),rdn(rdnn(D1),O1),rdn(rdnn(RD),RO)) ),
inference(fof_nnf,[status(thm)],[add_rdn_digit_rdn]) ).
fof(f_301_2,plain,
! [U_134,U_133,U_132,U_131,U_130,U_129] :
( rdn_add_with_carry(rdnn(U_134),rdn(rdnn(U_133),U_132),rdnn(U_131),rdn(rdnn(U_130),U_129))
| ~ rdn_add_with_carry(rdnn(U_134),rdnn(U_131),rdn(rdnn(U_133),U_132),rdn(rdnn(U_130),U_129)) ),
inference(variable_rename,[status(thm)],[f_301_1]) ).
cnf(f_301_3,plain,
( rdn_add_with_carry(rdnn(U_134),rdn(rdnn(U_133),U_132),rdnn(U_131),rdn(rdnn(U_130),U_129))
| ~ rdn_add_with_carry(rdnn(U_134),rdnn(U_131),rdn(rdnn(U_133),U_132),rdn(rdnn(U_130),U_129)) ),
inference(clausify,[status(thm)],[f_301_2]) ).
fof(f_302_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n0_n0_n0]) ).
cnf(f_302_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
inference(clausify,[status(thm)],[f_302_1]) ).
fof(f_303_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(n1),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n1_n1_n0]) ).
cnf(f_303_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(n1),rdnn(n0)),
inference(clausify,[status(thm)],[f_303_1]) ).
fof(f_304_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(n2),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n2_n2_n0]) ).
cnf(f_304_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(n2),rdnn(n0)),
inference(clausify,[status(thm)],[f_304_1]) ).
fof(f_305_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n3),rdnn(n3),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n3_n3_n0]) ).
cnf(f_305_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n3),rdnn(n3),rdnn(n0)),
inference(clausify,[status(thm)],[f_305_1]) ).
fof(f_306_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n4),rdnn(n4),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n4_n4_n0]) ).
cnf(f_306_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n4),rdnn(n4),rdnn(n0)),
inference(clausify,[status(thm)],[f_306_1]) ).
fof(f_307_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n5),rdnn(n5),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n5_n5_n0]) ).
cnf(f_307_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n5),rdnn(n5),rdnn(n0)),
inference(clausify,[status(thm)],[f_307_1]) ).
fof(f_308_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n6),rdnn(n6),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n6_n6_n0]) ).
cnf(f_308_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n6),rdnn(n6),rdnn(n0)),
inference(clausify,[status(thm)],[f_308_1]) ).
fof(f_309_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n7),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n7_n7_n0]) ).
cnf(f_309_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n7),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_309_1]) ).
fof(f_310_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n8),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n8_n8_n0]) ).
cnf(f_310_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n8),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_310_1]) ).
fof(f_311_1,plain,
rdn_digit_add(rdnn(n0),rdnn(n9),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n0_n9_n9_n0]) ).
cnf(f_311_2,plain,
rdn_digit_add(rdnn(n0),rdnn(n9),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_311_1]) ).
fof(f_312_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n0_n1_n0]) ).
cnf(f_312_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)),
inference(clausify,[status(thm)],[f_312_1]) ).
fof(f_313_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n1),rdnn(n2),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n1_n2_n0]) ).
cnf(f_313_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n1),rdnn(n2),rdnn(n0)),
inference(clausify,[status(thm)],[f_313_1]) ).
fof(f_314_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n2),rdnn(n3),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n2_n3_n0]) ).
cnf(f_314_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n2),rdnn(n3),rdnn(n0)),
inference(clausify,[status(thm)],[f_314_1]) ).
fof(f_315_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n3),rdnn(n4),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n3_n4_n0]) ).
cnf(f_315_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n3),rdnn(n4),rdnn(n0)),
inference(clausify,[status(thm)],[f_315_1]) ).
fof(f_316_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n4),rdnn(n5),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n4_n5_n0]) ).
cnf(f_316_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n4),rdnn(n5),rdnn(n0)),
inference(clausify,[status(thm)],[f_316_1]) ).
fof(f_317_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n5),rdnn(n6),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n5_n6_n0]) ).
cnf(f_317_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n5),rdnn(n6),rdnn(n0)),
inference(clausify,[status(thm)],[f_317_1]) ).
fof(f_318_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n6),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n6_n7_n0]) ).
cnf(f_318_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n6),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_318_1]) ).
fof(f_319_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n7_n8_n0]) ).
cnf(f_319_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_319_1]) ).
fof(f_320_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n8),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n8_n9_n0]) ).
cnf(f_320_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n8),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_320_1]) ).
fof(f_321_1,plain,
rdn_digit_add(rdnn(n1),rdnn(n9),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n1_n9_n0_n1]) ).
cnf(f_321_2,plain,
rdn_digit_add(rdnn(n1),rdnn(n9),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_321_1]) ).
fof(f_322_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n0_n2_n0]) ).
cnf(f_322_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(n0)),
inference(clausify,[status(thm)],[f_322_1]) ).
fof(f_323_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n1),rdnn(n3),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n1_n3_n0]) ).
cnf(f_323_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n1),rdnn(n3),rdnn(n0)),
inference(clausify,[status(thm)],[f_323_1]) ).
fof(f_324_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n2),rdnn(n4),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n2_n4_n0]) ).
cnf(f_324_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n2),rdnn(n4),rdnn(n0)),
inference(clausify,[status(thm)],[f_324_1]) ).
fof(f_325_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n3),rdnn(n5),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n3_n5_n0]) ).
cnf(f_325_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n3),rdnn(n5),rdnn(n0)),
inference(clausify,[status(thm)],[f_325_1]) ).
fof(f_326_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n4),rdnn(n6),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n4_n6_n0]) ).
cnf(f_326_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n4),rdnn(n6),rdnn(n0)),
inference(clausify,[status(thm)],[f_326_1]) ).
fof(f_327_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n5),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n5_n7_n0]) ).
cnf(f_327_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n5),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_327_1]) ).
fof(f_328_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n6),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n6_n8_n0]) ).
cnf(f_328_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n6),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_328_1]) ).
fof(f_329_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n7),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n7_n9_n0]) ).
cnf(f_329_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n7),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_329_1]) ).
fof(f_330_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n8),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n8_n0_n1]) ).
cnf(f_330_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n8),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_330_1]) ).
fof(f_331_1,plain,
rdn_digit_add(rdnn(n2),rdnn(n9),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n2_n9_n1_n1]) ).
cnf(f_331_2,plain,
rdn_digit_add(rdnn(n2),rdnn(n9),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_331_1]) ).
fof(f_332_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n0),rdnn(n3),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n0_n3_n0]) ).
cnf(f_332_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n0),rdnn(n3),rdnn(n0)),
inference(clausify,[status(thm)],[f_332_1]) ).
fof(f_333_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n1),rdnn(n4),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n1_n4_n0]) ).
cnf(f_333_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n1),rdnn(n4),rdnn(n0)),
inference(clausify,[status(thm)],[f_333_1]) ).
fof(f_334_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n2),rdnn(n5),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n2_n5_n0]) ).
cnf(f_334_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n2),rdnn(n5),rdnn(n0)),
inference(clausify,[status(thm)],[f_334_1]) ).
fof(f_335_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n3),rdnn(n6),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n3_n6_n0]) ).
cnf(f_335_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n3),rdnn(n6),rdnn(n0)),
inference(clausify,[status(thm)],[f_335_1]) ).
fof(f_336_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n4),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n4_n7_n0]) ).
cnf(f_336_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n4),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_336_1]) ).
fof(f_337_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n5),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n5_n8_n0]) ).
cnf(f_337_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n5),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_337_1]) ).
fof(f_338_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n6),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n6_n9_n0]) ).
cnf(f_338_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n6),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_338_1]) ).
fof(f_339_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n7),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n7_n0_n1]) ).
cnf(f_339_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n7),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_339_1]) ).
fof(f_340_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n8),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n8_n1_n1]) ).
cnf(f_340_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n8),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_340_1]) ).
fof(f_341_1,plain,
rdn_digit_add(rdnn(n3),rdnn(n9),rdnn(n2),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n3_n9_n2_n1]) ).
cnf(f_341_2,plain,
rdn_digit_add(rdnn(n3),rdnn(n9),rdnn(n2),rdnn(n1)),
inference(clausify,[status(thm)],[f_341_1]) ).
fof(f_342_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n0),rdnn(n4),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n0_n4_n0]) ).
cnf(f_342_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n0),rdnn(n4),rdnn(n0)),
inference(clausify,[status(thm)],[f_342_1]) ).
fof(f_343_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n1),rdnn(n5),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n1_n5_n0]) ).
cnf(f_343_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n1),rdnn(n5),rdnn(n0)),
inference(clausify,[status(thm)],[f_343_1]) ).
fof(f_344_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n2),rdnn(n6),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n2_n6_n0]) ).
cnf(f_344_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n2),rdnn(n6),rdnn(n0)),
inference(clausify,[status(thm)],[f_344_1]) ).
fof(f_345_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n3),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n3_n7_n0]) ).
cnf(f_345_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n3),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_345_1]) ).
fof(f_346_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n4),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n4_n8_n0]) ).
cnf(f_346_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n4),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_346_1]) ).
fof(f_347_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n5),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n5_n9_n0]) ).
cnf(f_347_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n5),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_347_1]) ).
fof(f_348_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n6),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n6_n0_n1]) ).
cnf(f_348_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n6),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_348_1]) ).
fof(f_349_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n7),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n7_n1_n1]) ).
cnf(f_349_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n7),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_349_1]) ).
fof(f_350_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n8),rdnn(n2),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n8_n2_n1]) ).
cnf(f_350_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n8),rdnn(n2),rdnn(n1)),
inference(clausify,[status(thm)],[f_350_1]) ).
fof(f_351_1,plain,
rdn_digit_add(rdnn(n4),rdnn(n9),rdnn(n3),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n4_n9_n3_n1]) ).
cnf(f_351_2,plain,
rdn_digit_add(rdnn(n4),rdnn(n9),rdnn(n3),rdnn(n1)),
inference(clausify,[status(thm)],[f_351_1]) ).
fof(f_352_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n0),rdnn(n5),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n0_n5_n0]) ).
cnf(f_352_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n0),rdnn(n5),rdnn(n0)),
inference(clausify,[status(thm)],[f_352_1]) ).
fof(f_353_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n1),rdnn(n6),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n1_n6_n0]) ).
cnf(f_353_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n1),rdnn(n6),rdnn(n0)),
inference(clausify,[status(thm)],[f_353_1]) ).
fof(f_354_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n2),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n2_n7_n0]) ).
cnf(f_354_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n2),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_354_1]) ).
fof(f_355_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n3),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n3_n8_n0]) ).
cnf(f_355_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n3),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_355_1]) ).
fof(f_356_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n4),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n4_n9_n0]) ).
cnf(f_356_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n4),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_356_1]) ).
fof(f_357_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n5),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n5_n0_n1]) ).
cnf(f_357_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n5),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_357_1]) ).
fof(f_358_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n6),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n6_n1_n1]) ).
cnf(f_358_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n6),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_358_1]) ).
fof(f_359_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n7),rdnn(n2),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n7_n2_n1]) ).
cnf(f_359_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n7),rdnn(n2),rdnn(n1)),
inference(clausify,[status(thm)],[f_359_1]) ).
fof(f_360_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n8),rdnn(n3),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n8_n3_n1]) ).
cnf(f_360_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n8),rdnn(n3),rdnn(n1)),
inference(clausify,[status(thm)],[f_360_1]) ).
fof(f_361_1,plain,
rdn_digit_add(rdnn(n5),rdnn(n9),rdnn(n4),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n5_n9_n4_n1]) ).
cnf(f_361_2,plain,
rdn_digit_add(rdnn(n5),rdnn(n9),rdnn(n4),rdnn(n1)),
inference(clausify,[status(thm)],[f_361_1]) ).
fof(f_362_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n0),rdnn(n6),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n0_n6_n0]) ).
cnf(f_362_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n0),rdnn(n6),rdnn(n0)),
inference(clausify,[status(thm)],[f_362_1]) ).
fof(f_363_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n1),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n1_n7_n0]) ).
cnf(f_363_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n1),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_363_1]) ).
fof(f_364_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n2),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n2_n8_n0]) ).
cnf(f_364_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n2),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_364_1]) ).
fof(f_365_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n3),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n3_n9_n0]) ).
cnf(f_365_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n3),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_365_1]) ).
fof(f_366_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n4),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n4_n0_n1]) ).
cnf(f_366_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n4),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_366_1]) ).
fof(f_367_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n5),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n5_n1_n1]) ).
cnf(f_367_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n5),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_367_1]) ).
fof(f_368_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n6),rdnn(n2),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n6_n2_n1]) ).
cnf(f_368_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n6),rdnn(n2),rdnn(n1)),
inference(clausify,[status(thm)],[f_368_1]) ).
fof(f_369_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n7),rdnn(n3),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n7_n3_n1]) ).
cnf(f_369_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n7),rdnn(n3),rdnn(n1)),
inference(clausify,[status(thm)],[f_369_1]) ).
fof(f_370_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n8),rdnn(n4),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n8_n4_n1]) ).
cnf(f_370_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n8),rdnn(n4),rdnn(n1)),
inference(clausify,[status(thm)],[f_370_1]) ).
fof(f_371_1,plain,
rdn_digit_add(rdnn(n6),rdnn(n9),rdnn(n5),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n6_n9_n5_n1]) ).
cnf(f_371_2,plain,
rdn_digit_add(rdnn(n6),rdnn(n9),rdnn(n5),rdnn(n1)),
inference(clausify,[status(thm)],[f_371_1]) ).
fof(f_372_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n0),rdnn(n7),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n0_n7_n0]) ).
cnf(f_372_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n0),rdnn(n7),rdnn(n0)),
inference(clausify,[status(thm)],[f_372_1]) ).
fof(f_373_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n1),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n1_n8_n0]) ).
cnf(f_373_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n1),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_373_1]) ).
fof(f_374_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n2),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n2_n9_n0]) ).
cnf(f_374_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n2),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_374_1]) ).
fof(f_375_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n3),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n3_n0_n1]) ).
cnf(f_375_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n3),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_375_1]) ).
fof(f_376_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n4),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n4_n1_n1]) ).
cnf(f_376_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n4),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_376_1]) ).
fof(f_377_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n5),rdnn(n2),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n5_n2_n1]) ).
cnf(f_377_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n5),rdnn(n2),rdnn(n1)),
inference(clausify,[status(thm)],[f_377_1]) ).
fof(f_378_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n6),rdnn(n3),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n6_n3_n1]) ).
cnf(f_378_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n6),rdnn(n3),rdnn(n1)),
inference(clausify,[status(thm)],[f_378_1]) ).
fof(f_379_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n7),rdnn(n4),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n7_n4_n1]) ).
cnf(f_379_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n7),rdnn(n4),rdnn(n1)),
inference(clausify,[status(thm)],[f_379_1]) ).
fof(f_380_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n8),rdnn(n5),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n8_n5_n1]) ).
cnf(f_380_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n8),rdnn(n5),rdnn(n1)),
inference(clausify,[status(thm)],[f_380_1]) ).
fof(f_381_1,plain,
rdn_digit_add(rdnn(n7),rdnn(n9),rdnn(n6),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n7_n9_n6_n1]) ).
cnf(f_381_2,plain,
rdn_digit_add(rdnn(n7),rdnn(n9),rdnn(n6),rdnn(n1)),
inference(clausify,[status(thm)],[f_381_1]) ).
fof(f_382_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(n8),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n0_n8_n0]) ).
cnf(f_382_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(n8),rdnn(n0)),
inference(clausify,[status(thm)],[f_382_1]) ).
fof(f_383_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n1),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n1_n9_n0]) ).
cnf(f_383_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n1),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_383_1]) ).
fof(f_384_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n2),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n2_n0_n1]) ).
cnf(f_384_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n2),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_384_1]) ).
fof(f_385_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n3),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n3_n1_n1]) ).
cnf(f_385_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n3),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_385_1]) ).
fof(f_386_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n4),rdnn(n2),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n4_n2_n1]) ).
cnf(f_386_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n4),rdnn(n2),rdnn(n1)),
inference(clausify,[status(thm)],[f_386_1]) ).
fof(f_387_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n5),rdnn(n3),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n5_n3_n1]) ).
cnf(f_387_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n5),rdnn(n3),rdnn(n1)),
inference(clausify,[status(thm)],[f_387_1]) ).
fof(f_388_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n6),rdnn(n4),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n6_n4_n1]) ).
cnf(f_388_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n6),rdnn(n4),rdnn(n1)),
inference(clausify,[status(thm)],[f_388_1]) ).
fof(f_389_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n7),rdnn(n5),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n7_n5_n1]) ).
cnf(f_389_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n7),rdnn(n5),rdnn(n1)),
inference(clausify,[status(thm)],[f_389_1]) ).
fof(f_390_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n8),rdnn(n6),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n8_n6_n1]) ).
cnf(f_390_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n8),rdnn(n6),rdnn(n1)),
inference(clausify,[status(thm)],[f_390_1]) ).
fof(f_391_1,plain,
rdn_digit_add(rdnn(n8),rdnn(n9),rdnn(n7),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n8_n9_n7_n1]) ).
cnf(f_391_2,plain,
rdn_digit_add(rdnn(n8),rdnn(n9),rdnn(n7),rdnn(n1)),
inference(clausify,[status(thm)],[f_391_1]) ).
fof(f_392_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n0),rdnn(n9),rdnn(n0)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n0_n9_n0]) ).
cnf(f_392_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n0),rdnn(n9),rdnn(n0)),
inference(clausify,[status(thm)],[f_392_1]) ).
fof(f_393_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n1),rdnn(n0),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n1_n0_n1]) ).
cnf(f_393_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n1),rdnn(n0),rdnn(n1)),
inference(clausify,[status(thm)],[f_393_1]) ).
fof(f_394_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n2),rdnn(n1),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n2_n1_n1]) ).
cnf(f_394_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n2),rdnn(n1),rdnn(n1)),
inference(clausify,[status(thm)],[f_394_1]) ).
fof(f_395_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n3),rdnn(n2),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n3_n2_n1]) ).
cnf(f_395_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n3),rdnn(n2),rdnn(n1)),
inference(clausify,[status(thm)],[f_395_1]) ).
fof(f_396_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n4),rdnn(n3),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n4_n3_n1]) ).
cnf(f_396_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n4),rdnn(n3),rdnn(n1)),
inference(clausify,[status(thm)],[f_396_1]) ).
fof(f_397_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n5),rdnn(n4),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n5_n4_n1]) ).
cnf(f_397_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n5),rdnn(n4),rdnn(n1)),
inference(clausify,[status(thm)],[f_397_1]) ).
fof(f_398_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n6),rdnn(n5),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n6_n5_n1]) ).
cnf(f_398_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n6),rdnn(n5),rdnn(n1)),
inference(clausify,[status(thm)],[f_398_1]) ).
fof(f_399_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n7),rdnn(n6),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n7_n6_n1]) ).
cnf(f_399_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n7),rdnn(n6),rdnn(n1)),
inference(clausify,[status(thm)],[f_399_1]) ).
fof(f_400_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n8),rdnn(n7),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n8_n7_n1]) ).
cnf(f_400_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n8),rdnn(n7),rdnn(n1)),
inference(clausify,[status(thm)],[f_400_1]) ).
fof(f_401_1,plain,
rdn_digit_add(rdnn(n9),rdnn(n9),rdnn(n8),rdnn(n1)),
inference(fof_nnf,[status(thm)],[rdn_digit_add_n9_n9_n8_n1]) ).
cnf(f_401_2,plain,
rdn_digit_add(rdnn(n9),rdnn(n9),rdnn(n8),rdnn(n1)),
inference(clausify,[status(thm)],[f_401_1]) ).
fof(f_402_1,negated_conjecture,
~ ? [X] : difference(X,n0,X),
inference(negate,[status(cth)],[diff_zero_identity]) ).
fof(f_402_2,negated_conjecture,
! [X] : ~ difference(X,n0,X),
inference(fof_nnf,[status(thm)],[f_402_1]) ).
fof(f_402_3,negated_conjecture,
! [U_135] : ~ difference(U_135,n0,U_135),
inference(variable_rename,[status(thm)],[f_402_2]) ).
fof(f_402_4,negated_conjecture,
! [U_135] : ~ difference(U_135,n0,U_135),
inference(definitional_conversion,[status(esa)],[f_402_3]) ).
cnf(f_402_5,negated_conjecture,
~ difference(U_135,n0,U_135),
inference(clausify,[status(thm)],[f_402_4]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( rdnn(Eq_x_0) = rdnn(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( rdn_pos(Eq_x_0) = rdn_pos(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( rdn(Eq_x_0,Eq_x_1) = rdn(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( rdn_neg(Eq_x_0) = rdn_neg(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( rdn_translate(Eq_y_0,Eq_y_1)
| ~ rdn_translate(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_9,axiom,
( rdn_non_zero_digit(Eq_y_0)
| ~ rdn_non_zero_digit(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( rdn_positive_less(Eq_y_0,Eq_y_1)
| ~ rdn_positive_less(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( rdn_non_zero(Eq_y_0)
| ~ rdn_non_zero(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( less(Eq_y_0,Eq_y_1)
| ~ less(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( less_or_equal(Eq_y_0,Eq_y_1)
| ~ less_or_equal(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( sum(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sum(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( rdn_add_with_carry(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ rdn_add_with_carry(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( difference(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ difference(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( rdn_digit_add(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ rdn_digit_add(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM340+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 19 18:17:18 UTC 2026
% 0.11/0.37 % CPUTime :
% 13.79/14.12 % SZS status Theorem for theBenchmark
% 13.79/14.12 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------