missing CPF output for R-producing loop
for at least one NO, CeTA says UNSUPPORTED, and that's because matchbox crashes while printing the certificate
https://www.starexec.org/starexec/secure/details/pair.jsp?id=615271149
(RULES b b b -> , a ->= , ->= a a a b a a)
pure-matchbox +RTS -N8 -RTS -S strat/combi.strat cpf=True --cpf ~/tpdb/TPDB/SRS_Relative/Waldmann_23/size-10-alpha-2-num-56.xml
...
pure-matchbox: CPF.nopf: missing case for reason Nontermination
looping relative SRS derivation
loop on weak rules
Closure source : "b"
inside_sources: 10
target : "bbbbbbbbbbbbbaaabbbbabbabb"
steps : 10
maxwidth : 30
strict : True
last_rule_app_source : 0
last_rule_app_target : 15
reason : Notstoredtosavesomespace
produces strict redex(13, "aaa")
CallStack (from HasCallStack):
error, called at src/Matchbox/Proof/CPF.hs:123:8 in pure-matchbox-1.1-c9b64ab466047ef838e1246a1636547ee70d8d675e7d6292305932b369650eb3:Matchbox.Proof.CPF
Edited by waldmann