Skip to content

Infinite loop in EliminateMeta with seemingly unrelated option #56

@jrosain

Description

@jrosain

Description of the issue

The proof of the attached problem is instantaneous as long as we don't ask Goéland to print it. However, once we want to actually print the proof, Goéland goes into an infinite loop of EliminateMeta and never does print it.

Flags used

-proof

Small problem file to reproduce the bug

https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN000+1.p
EDIT: this also happens on https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN000_1.p

Version of Goéland where the issue occurs

v.1.2-dev.rc9841dae9e19c823410fa0e003a325f8ac1cd44b

Metadata

Metadata

Assignees

Labels

kind:bugSomething isn't workingpart:proof-outputAbout the vanilla proof output (in custom format)

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions