Annotated TSTP Formulae<language>(<name>,<role>, <formula>[, <source>[, <useful info>]]). BNF Online | Example FOF Problem Formulafof(subclass_defn,axiom, ! [X,Y] : ( subclass(X,Y) <=> ! [U] : ( member(U,X) => member(U,Y) ) ), file('SET005+0.ax',subclass_defn), [description('Definition of subclass'), relevance(0.9)]). Example CNF Solution Formulacnf(140,derived-lemma, ( equal_sets(a,aUa) | member(member_of(a,aUa),a) ), inference(unit_del,[status(thm)],[ inference(hyper,[status(thm)],[ 5,16]),11]), [iquote('hyper,5,16.1,unit_del,11')]). |