fof(nn,axiom, (((rdftype(n0, ind))))).
fof(nn,axiom, ! [A] : ((rdftype(n0, A)) => ((rdftype(n1, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n0, A)) => ((rdftype(i1, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n0, A)) => ((rdftype(j1, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n1, A)) => ((rdftype(n2, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n1, A)) => ((rdftype(i2, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n1, A)) => ((rdftype(j2, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n2, A)) => ((rdftype(n3, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n2, A)) => ((rdftype(i3, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n2, A)) => ((rdftype(j3, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n3, A)) => ((rdftype(n4, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n3, A)) => ((rdftype(i4, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n3, A)) => ((rdftype(j4, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n4, A)) => ((rdftype(n5, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n4, A)) => ((rdftype(i5, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n4, A)) => ((rdftype(j5, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n5, A)) => ((rdftype(n6, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n5, A)) => ((rdftype(i6, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n5, A)) => ((rdftype(j6, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n6, A)) => ((rdftype(n7, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n6, A)) => ((rdftype(i7, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n6, A)) => ((rdftype(j7, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n7, A)) => ((rdftype(n8, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n7, A)) => ((rdftype(i8, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n7, A)) => ((rdftype(j8, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n8, A)) => ((rdftype(n9, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n8, A)) => ((rdftype(i9, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n8, A)) => ((rdftype(j9, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n9, A)) => ((rdftype(n10, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n9, A)) => ((rdftype(i10, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n9, A)) => ((rdftype(j10, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n10, A)) => ((rdftype(n11, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n10, A)) => ((rdftype(i11, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n10, A)) => ((rdftype(j11, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n11, A)) => ((rdftype(n12, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n11, A)) => ((rdftype(i12, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n11, A)) => ((rdftype(j12, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n12, A)) => ((rdftype(n13, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n12, A)) => ((rdftype(i13, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n12, A)) => ((rdftype(j13, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n13, A)) => ((rdftype(n14, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n13, A)) => ((rdftype(i14, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n13, A)) => ((rdftype(j14, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n14, A)) => ((rdftype(n15, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n14, A)) => ((rdftype(i15, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n14, A)) => ((rdftype(j15, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n15, A)) => ((rdftype(n16, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n15, A)) => ((rdftype(i16, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n15, A)) => ((rdftype(j16, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n16, A)) => ((rdftype(n17, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n16, A)) => ((rdftype(i17, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n16, A)) => ((rdftype(j17, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n17, A)) => ((rdftype(n18, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n17, A)) => ((rdftype(i18, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n17, A)) => ((rdftype(j18, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n18, A)) => ((rdftype(n19, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n18, A)) => ((rdftype(i19, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n18, A)) => ((rdftype(j19, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n19, A)) => ((rdftype(n20, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n19, A)) => ((rdftype(i20, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n19, A)) => ((rdftype(j20, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n20, A)) => ((rdftype(n21, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n20, A)) => ((rdftype(i21, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n20, A)) => ((rdftype(j21, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n21, A)) => ((rdftype(n22, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n21, A)) => ((rdftype(i22, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n21, A)) => ((rdftype(j22, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n22, A)) => ((rdftype(n23, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n22, A)) => ((rdftype(i23, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n22, A)) => ((rdftype(j23, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n23, A)) => ((rdftype(n24, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n23, A)) => ((rdftype(i24, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n23, A)) => ((rdftype(j24, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n24, A)) => ((rdftype(n25, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n24, A)) => ((rdftype(i25, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n24, A)) => ((rdftype(j25, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n25, A)) => ((rdftype(n26, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n25, A)) => ((rdftype(i26, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n25, A)) => ((rdftype(j26, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n26, A)) => ((rdftype(n27, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n26, A)) => ((rdftype(i27, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n26, A)) => ((rdftype(j27, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n27, A)) => ((rdftype(n28, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n27, A)) => ((rdftype(i28, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n27, A)) => ((rdftype(j28, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n28, A)) => ((rdftype(n29, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n28, A)) => ((rdftype(i29, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n28, A)) => ((rdftype(j29, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n29, A)) => ((rdftype(n30, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n29, A)) => ((rdftype(i30, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n29, A)) => ((rdftype(j30, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n30, A)) => ((rdftype(n31, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n30, A)) => ((rdftype(i31, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n30, A)) => ((rdftype(j31, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n31, A)) => ((rdftype(n32, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n31, A)) => ((rdftype(i32, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n31, A)) => ((rdftype(j32, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n32, A)) => ((rdftype(n33, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n32, A)) => ((rdftype(i33, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n32, A)) => ((rdftype(j33, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n33, A)) => ((rdftype(n34, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n33, A)) => ((rdftype(i34, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n33, A)) => ((rdftype(j34, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n34, A)) => ((rdftype(n35, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n34, A)) => ((rdftype(i35, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n34, A)) => ((rdftype(j35, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n35, A)) => ((rdftype(n36, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n35, A)) => ((rdftype(i36, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n35, A)) => ((rdftype(j36, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n36, A)) => ((rdftype(n37, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n36, A)) => ((rdftype(i37, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n36, A)) => ((rdftype(j37, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n37, A)) => ((rdftype(n38, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n37, A)) => ((rdftype(i38, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n37, A)) => ((rdftype(j38, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n38, A)) => ((rdftype(n39, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n38, A)) => ((rdftype(i39, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n38, A)) => ((rdftype(j39, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n39, A)) => ((rdftype(n40, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n39, A)) => ((rdftype(i40, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n39, A)) => ((rdftype(j40, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n40, A)) => ((rdftype(n41, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n40, A)) => ((rdftype(i41, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n40, A)) => ((rdftype(j41, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n41, A)) => ((rdftype(n42, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n41, A)) => ((rdftype(i42, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n41, A)) => ((rdftype(j42, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n42, A)) => ((rdftype(n43, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n42, A)) => ((rdftype(i43, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n42, A)) => ((rdftype(j43, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n43, A)) => ((rdftype(n44, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n43, A)) => ((rdftype(i44, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n43, A)) => ((rdftype(j44, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n44, A)) => ((rdftype(n45, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n44, A)) => ((rdftype(i45, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n44, A)) => ((rdftype(j45, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n45, A)) => ((rdftype(n46, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n45, A)) => ((rdftype(i46, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n45, A)) => ((rdftype(j46, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n46, A)) => ((rdftype(n47, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n46, A)) => ((rdftype(i47, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n46, A)) => ((rdftype(j47, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n47, A)) => ((rdftype(n48, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n47, A)) => ((rdftype(i48, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n47, A)) => ((rdftype(j48, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n48, A)) => ((rdftype(n49, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n48, A)) => ((rdftype(i49, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n48, A)) => ((rdftype(j49, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n49, A)) => ((rdftype(n50, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n49, A)) => ((rdftype(i50, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n49, A)) => ((rdftype(j50, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n50, A)) => ((rdftype(n51, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n50, A)) => ((rdftype(i51, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n50, A)) => ((rdftype(j51, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n51, A)) => ((rdftype(n52, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n51, A)) => ((rdftype(i52, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n51, A)) => ((rdftype(j52, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n52, A)) => ((rdftype(n53, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n52, A)) => ((rdftype(i53, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n52, A)) => ((rdftype(j53, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n53, A)) => ((rdftype(n54, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n53, A)) => ((rdftype(i54, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n53, A)) => ((rdftype(j54, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n54, A)) => ((rdftype(n55, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n54, A)) => ((rdftype(i55, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n54, A)) => ((rdftype(j55, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n55, A)) => ((rdftype(n56, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n55, A)) => ((rdftype(i56, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n55, A)) => ((rdftype(j56, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n56, A)) => ((rdftype(n57, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n56, A)) => ((rdftype(i57, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n56, A)) => ((rdftype(j57, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n57, A)) => ((rdftype(n58, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n57, A)) => ((rdftype(i58, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n57, A)) => ((rdftype(j58, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n58, A)) => ((rdftype(n59, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n58, A)) => ((rdftype(i59, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n58, A)) => ((rdftype(j59, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n59, A)) => ((rdftype(n60, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n59, A)) => ((rdftype(i60, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n59, A)) => ((rdftype(j60, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n60, A)) => ((rdftype(n61, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n60, A)) => ((rdftype(i61, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n60, A)) => ((rdftype(j61, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n61, A)) => ((rdftype(n62, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n61, A)) => ((rdftype(i62, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n61, A)) => ((rdftype(j62, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n62, A)) => ((rdftype(n63, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n62, A)) => ((rdftype(i63, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n62, A)) => ((rdftype(j63, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n63, A)) => ((rdftype(n64, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n63, A)) => ((rdftype(i64, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n63, A)) => ((rdftype(j64, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n64, A)) => ((rdftype(n65, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n64, A)) => ((rdftype(i65, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n64, A)) => ((rdftype(j65, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n65, A)) => ((rdftype(n66, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n65, A)) => ((rdftype(i66, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n65, A)) => ((rdftype(j66, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n66, A)) => ((rdftype(n67, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n66, A)) => ((rdftype(i67, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n66, A)) => ((rdftype(j67, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n67, A)) => ((rdftype(n68, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n67, A)) => ((rdftype(i68, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n67, A)) => ((rdftype(j68, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n68, A)) => ((rdftype(n69, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n68, A)) => ((rdftype(i69, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n68, A)) => ((rdftype(j69, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n69, A)) => ((rdftype(n70, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n69, A)) => ((rdftype(i70, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n69, A)) => ((rdftype(j70, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n70, A)) => ((rdftype(n71, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n70, A)) => ((rdftype(i71, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n70, A)) => ((rdftype(j71, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n71, A)) => ((rdftype(n72, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n71, A)) => ((rdftype(i72, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n71, A)) => ((rdftype(j72, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n72, A)) => ((rdftype(n73, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n72, A)) => ((rdftype(i73, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n72, A)) => ((rdftype(j73, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n73, A)) => ((rdftype(n74, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n73, A)) => ((rdftype(i74, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n73, A)) => ((rdftype(j74, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n74, A)) => ((rdftype(n75, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n74, A)) => ((rdftype(i75, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n74, A)) => ((rdftype(j75, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n75, A)) => ((rdftype(n76, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n75, A)) => ((rdftype(i76, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n75, A)) => ((rdftype(j76, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n76, A)) => ((rdftype(n77, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n76, A)) => ((rdftype(i77, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n76, A)) => ((rdftype(j77, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n77, A)) => ((rdftype(n78, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n77, A)) => ((rdftype(i78, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n77, A)) => ((rdftype(j78, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n78, A)) => ((rdftype(n79, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n78, A)) => ((rdftype(i79, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n78, A)) => ((rdftype(j79, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n79, A)) => ((rdftype(n80, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n79, A)) => ((rdftype(i80, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n79, A)) => ((rdftype(j80, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n80, A)) => ((rdftype(n81, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n80, A)) => ((rdftype(i81, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n80, A)) => ((rdftype(j81, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n81, A)) => ((rdftype(n82, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n81, A)) => ((rdftype(i82, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n81, A)) => ((rdftype(j82, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n82, A)) => ((rdftype(n83, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n82, A)) => ((rdftype(i83, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n82, A)) => ((rdftype(j83, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n83, A)) => ((rdftype(n84, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n83, A)) => ((rdftype(i84, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n83, A)) => ((rdftype(j84, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n84, A)) => ((rdftype(n85, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n84, A)) => ((rdftype(i85, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n84, A)) => ((rdftype(j85, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n85, A)) => ((rdftype(n86, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n85, A)) => ((rdftype(i86, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n85, A)) => ((rdftype(j86, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n86, A)) => ((rdftype(n87, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n86, A)) => ((rdftype(i87, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n86, A)) => ((rdftype(j87, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n87, A)) => ((rdftype(n88, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n87, A)) => ((rdftype(i88, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n87, A)) => ((rdftype(j88, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n88, A)) => ((rdftype(n89, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n88, A)) => ((rdftype(i89, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n88, A)) => ((rdftype(j89, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n89, A)) => ((rdftype(n90, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n89, A)) => ((rdftype(i90, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n89, A)) => ((rdftype(j90, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n90, A)) => ((rdftype(n91, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n90, A)) => ((rdftype(i91, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n90, A)) => ((rdftype(j91, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n91, A)) => ((rdftype(n92, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n91, A)) => ((rdftype(i92, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n91, A)) => ((rdftype(j92, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n92, A)) => ((rdftype(n93, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n92, A)) => ((rdftype(i93, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n92, A)) => ((rdftype(j93, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n93, A)) => ((rdftype(n94, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n93, A)) => ((rdftype(i94, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n93, A)) => ((rdftype(j94, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n94, A)) => ((rdftype(n95, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n94, A)) => ((rdftype(i95, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n94, A)) => ((rdftype(j95, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n95, A)) => ((rdftype(n96, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n95, A)) => ((rdftype(i96, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n95, A)) => ((rdftype(j96, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n96, A)) => ((rdftype(n97, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n96, A)) => ((rdftype(i97, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n96, A)) => ((rdftype(j97, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n97, A)) => ((rdftype(n98, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n97, A)) => ((rdftype(i98, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n97, A)) => ((rdftype(j98, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n98, A)) => ((rdftype(n99, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n98, A)) => ((rdftype(i99, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n98, A)) => ((rdftype(j99, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n99, A)) => ((rdftype(n100, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n99, A)) => ((rdftype(i100, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n99, A)) => ((rdftype(j100, A))))).
fof(nn,axiom, ! [A] : ((rdftype(n100, A)) => ((rdftype(a2, A))))).
fof(nn,axiom, ! [A] : ((rdftype(a2, A)) => ((goal)))).
fof(goal_to_be_proved,conjecture,goal).