Home
last modified time | relevance | path

Searched refs:CPTypeNegConjecture (Results 1 – 9 of 9) sorted by relevance

/dports/math/eprover/eprover-E-2.0/CLAUSES/
H A Dccl_formula_wrapper.c279 type = CPTypeNegConjecture; in WFormulaTPTPParse()
329 case CPTypeNegConjecture: in WFormulaTPTPPrint()
485 case CPTypeNegConjecture: in WFormulaTSTPPrint()
H A Dccl_formula_wrapper.h75 ((FormulaQueryType(form)==CPTypeNegConjecture) || \
H A Dccl_clauses.c1340 case CPTypeNegConjecture: in ClausePrintTPTPFormat()
1384 (ClauseQueryTPTPType(clause) == CPTypeNegConjecture) )&& in ClausePrintLOPFormat()
1562 case CPTypeNegConjecture: in ClauseTSTPPrint()
1670 res = CPTypeNegConjecture; in ClauseTypeParse()
1735 type = CPTypeNegConjecture; /* Old TPTP syntax lies ;-) */ in ClauseParse()
1806 type = CPTypeNegConjecture; in ClauseParse()
H A Dccl_clauses.h78 CPTypeNegConjecture = CPType1|CPType3, /* Clause is an negated enumerator
246 ((ClauseQueryTPTPType(clause)==CPTypeNegConjecture) ||\
H A Dccl_derivation.c1402 case CPTypeNegConjecture: in DerivedDotNodeColour()
1415 case CPTypeNegConjecture: in DerivedDotNodeColour()
H A Dccl_formulafunc.c256 FormulaSetType(wform, CPTypeNegConjecture); in WFormulaConjectureNegate()
H A Dccl_inferencedoc.c73 case CPTypeNegConjecture: in PCLTypeStr()
/dports/math/eprover/eprover-E-2.0/PCL2/
H A Dpcl_steps.h59 PCLTypeNegConjecture = CPTypeNegConjecture, /* Formula is NegConjecture */
/dports/math/eprover/eprover-E-2.0/HEURISTICS/
H A Dche_funweights.c77 if(ClauseQueryTPTPType(handle)==CPTypeNegConjecture) in init_conj_vector()