Stop ignoring negated conjecture in problems

devtools/test-suite/bugs/bug_66-1.p

@@ -0,0 +1,4 @@
+% result: VALID
+
+fof(h, hypothesis, p ).
+fof(nc, negated_conjecture, ~p ).

devtools/test-suite/bugs/bug_66-2.p

@@ -0,0 +1,4 @@
+% result: NOT VALID
+
+fof(h, hypothesis, p ).
+fof(nc, negated_conjecture, p ).

src/main.go

@@ -207,7 +207,7 @@ func initDebuggers() {
 
 func StatementListToFormula(statements []Core.Statement, old_bound int, problemDir string) (form AST.Form, bound int, containsEquality bool) {
 	and_list := AST.NewFormList()
-	var not_form AST.Form
+	var negated_conjecture AST.Form
 	bound = old_bound
 
 	for _, statement := range statements {
@@ -249,31 +249,42 @@ func StatementListToFormula(statements []Core.Statement, old_bound int, problemD
 		case Core.Conjecture:
 			switch f := statement.GetForm().(type) {
 			case Lib.Some[AST.Form]:
-				not_form = doConjectureStatement(f.Val)
+				negated_conjecture = AST.MakerNot(doConjectureStatement(f.Val))
 			case Lib.None[AST.Form]:
 				Glob.Anomaly("main", "Conjecture statement "+statement.ToString()+" has no formula")
 			}
 
+		case Core.NegatedConjecture:
+			switch f := statement.GetForm().(type) {
+			case Lib.Some[AST.Form]:
+				negated_conjecture = doConjectureStatement(f.Val)
+			case Lib.None[AST.Form]:
+				Glob.Anomaly("main", "Negated conjecture statement "+statement.ToString()+" has no formula")
+			}
+
 		case Core.Type:
 			switch ty := statement.GetAtomTyping().(type) {
 			case Lib.Some[Core.TFFAtomTyping]:
 				doTypeStatement(ty.Val)
 			case Lib.None[Core.TFFAtomTyping]:
 				Glob.Anomaly("main", "Type statement "+statement.ToString()+" has no formula")
 			}
+
+		default:
+			Glob.Fatal("main", fmt.Sprintf("Unmanaged statement role: %s", statement.GetRole().ToString()))
 		}
 	}
 
 	switch {
-	case and_list.IsEmpty() && not_form == nil:
+	case and_list.IsEmpty() && negated_conjecture == nil:
 		return nil, bound, containsEquality
 	case and_list.IsEmpty():
-		return AST.MakerNot(not_form), bound, containsEquality
-	case not_form == nil:
+		return negated_conjecture, bound, containsEquality
+	case negated_conjecture == nil:
 		return AST.MakerAnd(and_list), bound, containsEquality
 	default:
 		flattened := and_list.Flatten()
-		flattened.Append(AST.MakerNot(not_form))
+		flattened.Append(negated_conjecture)
 		return AST.MakerAnd(flattened), bound, containsEquality
 	}
 }