diff --git a/devtools/run-test-suite.py b/devtools/run-test-suite.py index 2b377173..433ce311 100644 --- a/devtools/run-test-suite.py +++ b/devtools/run-test-suite.py @@ -122,7 +122,7 @@ def compareOutputs(f, parser): for f in glob.glob("test-suite/**/*.p"): parser = Parser(f) - if any(out in parser.arguments for out in outputTest) : + if any(out in parser.arguments for out in outputTest) and (os.path.exists(os.path.splitext(f)[0] + ".out")) : compareOutputs(f, parser) else : runWithExpected(f, parser) diff --git a/devtools/test-suite/bugs/bug_61.p b/devtools/test-suite/bugs/bug_61.p new file mode 100644 index 00000000..8ace4b94 --- /dev/null +++ b/devtools/test-suite/bugs/bug_61.p @@ -0,0 +1,37 @@ +% args: -otptp +% result: VALID + +%------------------------------------------------------------------------------ +fof(c1, axiom, + ! [X] : + (q(b) + | ~ s(X))). + +fof(c2, axiom, + ! [X] : + (~ q(b) + | ~ p(X) + | ~ r)). + +fof(c3, axiom, + (p(c) + | ~ q(c))). + +fof(c4, axiom, + ! [Y] : + (p(c) + | q(Y))). + +fof(c5, axiom, + (q(c) + | ~ q(b))). + +fof(c6, axiom, + (r + | ~ p(c))). + +fof(c7, axiom, + (s(sK1) + | q(b) + | ~ p(c))). +%------------------------------------------------------------------------------ diff --git a/src/Mods/tptp/proof.go b/src/Mods/tptp/proof.go index 83475561..d48b6426 100644 --- a/src/Mods/tptp/proof.go +++ b/src/Mods/tptp/proof.go @@ -498,7 +498,12 @@ func processMainFormula(form AST.Form) (*AST.FormList, AST.Form) { case AST.And: last := nf.FormList.Len() - 1 formList = AST.NewFormList(nf.FormList.GetElements(0, last)...) - form = nf.FormList.Get(last).(AST.Not).GetForm() + switch f := nf.FormList.Get(last).(type) { + case AST.Not: + form = f.GetForm() + default: + form = f + } } return formList, form }