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(a2, A))))).
fof(nn,axiom, ! [A] : ((rdftype(a2, A)) => ((goal)))).
fof(goal_to_be_proved,conjecture,goal).