Skip to content

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