- Join over
**1.5M+ people** - Join over
**100K+ communities** - Free
**without limits** - Create
**your own community**

- Jul 05 23:33Jenkins nightly build failure
- Jul 02 23:32Jenkins nightly build failure
- Jul 01 23:32Jenkins nightly build failure
- Jun 30 23:32Jenkins nightly build failure
- Jun 29 23:33Jenkins nightly build failure
- Jun 28 23:33Jenkins nightly build failure
- Jun 25 23:33Jenkins nightly build failure
- Jun 24 23:33Jenkins nightly build failure
- Jun 23 23:33Jenkins nightly build failure
- Jun 22 23:33Jenkins nightly build failure
- Jun 21 23:33Jenkins nightly build failure
- Jun 18 23:33Jenkins nightly build failure
- Jun 17 23:33Jenkins nightly build failure
- Jun 16 23:32Jenkins nightly build failure
- Jun 15 23:32Jenkins nightly build failure
- Jun 14 23:33Jenkins nightly build failure
- Jun 11 23:32Jenkins nightly build failure
- Jun 10 23:32Jenkins nightly build failure
- Jun 09 23:32Jenkins nightly build failure
- Jun 08 23:32Jenkins nightly build failure

It looks like there is a much shorter proof. :-) Some data: in order to parse the proof, we convert it using

`prooftrans ivy`

. This blows the proof up to 22k inferences. The massive reduction then happens in `fixDerivation`

, where we add extra inferences to make sure that the input clauses match up with our clausification. Not sure why the proof gets smaller here.
Ok, found the bug. This was interesting. So as explained above, we parse the proof from the ivy format produced by *double* backslash.

`prooftrans ivy`

. However we parse the input formulas of the original problem directly from the prover9 file. Interestingly, backslashes are escaped in the ivy format---they are written as `backslash_for_ivy`

. The translation code was originally written by Martin many years ago and mapped the ivy backslash to a
Now

`fixDerivation`

found an input clause with two backslashes and couldn't find it in the end-sequent. So it called Escargot: please derive the clause with the double backslash. And Escargot returned a (very short) proof of the empty clause...
I think I should get rid of the backslashes

```
java.lang.OutOfMemoryError: Java heap space
at scala.collection.immutable.HashSet$HashTrieSet.updated0(HashSet.scala:554)
at scala.collection.immutable.HashSet.$plus(HashSet.scala:84)
at scala.collection.immutable.HashSet.$plus(HashSet.scala:35)
at scala.collection.mutable.SetBuilder.$plus$eq(SetBuilder.scala:28)
at scala.collection.mutable.SetBuilder.$plus$eq(SetBuilder.scala:24)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:237)
at scala.collection.TraversableLike$$Lambda$74/1911152052.apply(Unknown Source)
```

How do I increase the heap space when running gapt?

I have been running the following

`Prover9Importer.expansionProof("Mich.pf")`

for a little less than an hour

So there are proof where a pi_1 cut seems not to exist

I mean pi_1 with 1 quantifier prefix

so I try to introduce a pi_1 cut with a 2 quantifier prefix

which works

but one of the quantifiers does not do anything, i.e. it does not appear in the formula

any idea why

here is the JSON

```
{
"0" : {"name" : "LogicalAxiom", "A" : "v0 / K(v2, v1) * K(v2, v1) = v0"},
"1" : {
"name" : "ForallLeftRule",
"subProof" : 0,
"aux" : -1,
"A" : "v0 / v1_0 * v1_0 = v0",
"term" : "K(v2, v1)",
"v" : "v1_0"
},
"2" : {
"name" : "ForallLeftRule",
"subProof" : 1,
"aux" : -1,
"A" : "∀v1_0 v0_0 / v1_0 * v1_0 = v0_0",
"term" : "v0",
"v" : "v0_0"
},
"3" : {"name" : "LogicalAxiom", "A" : "K(v2, v1) * 1 = K(v2, v1)"},
"4" : {
"name" : "ForallLeftRule",
"subProof" : 3,
"aux" : -1,
"A" : "v0_0 * 1 = v0_0",
"term" : "K(v2, v1)",
"v" : "v0_0"
},
"5" : {
"name" : "LogicalAxiom",
"A" : "1 * (v0 / K(v2, v1) * K(v2, v1)) = v0 / K(v2, v1) * K(v2, v1)"
},
"6" : {
"name" : "ForallLeftRule",
"subProof" : 5,
"aux" : -1,
"A" : "1 * v0_0 = v0_0",
"term" : "v0 / K(v2, v1) * K(v2, v1)",
"v" : "v0_0"
},
"7" : {
"name" : "LogicalAxiom",
"A" : "v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1))) =\n v0 / K(v2, v1) * (K(v2, v1) * 1) * (v0 / K(v2, v1)) * K(v2, v1)"
},
"8" : {
"name" : "ForallLeftRule",
"subProof" : 7,
"aux" : -1,
"A" : "v0 / K(v2, v1) * K(v2, v1) * (v2_0 * (v0 / K(v2, v1) * K(v2, v1))) =\n v0 / K(v2, v1) * (K(v2, v1) * v2_0) * (v0 / K(v2, v1)) * K(v2, v1)",
"term" : "1",
"v" : "v2_0"
},
"9" : {
"name" : "ForallLeftRule",
"subProof" : 8,
"aux" : -1,
"A" : "∀v2_0\n v0 / K(v2, v1) * v1_0 * (v2_0 * (v0 / K(v2, v1) * v1_0)) =\n v0 / K(v2, v1) * (v1_0 * v2_0) * (v0 / K(v2, v1)) * v1_0",
"term" : "K(v2, v1)",
"v" : "v1_0"
},
"10" : {
"name" : "ForallLeftRule",
"subProof" : 9,
"aux" : -1,
"A" : "∀v1_0\n ∀v2_0\n v0_0 * v1_0 * (v2_0 * (v0_0 * v1_0)) = v0_0 * (v1_0 * v2_0) * v0_0 * v1_0",
"term" : "v0 / K(v2, v1)",
"v" : "v0_0"
},
"11" : {
"name" : "ReflexivityAxiom",
"s" : "v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1)))"
},
"12" : {
"name" : "WeakeningLeftRule",
"subProof" : 11,
"formula" : "v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1))) =\n v0 / K(v2, v1) * (K(v2, v1) * 1) * (v0 / K(v2, v1)) * K(v2, v1)"
},
"13" : {
"name" : "EqualityRightRule",
"subProof" : 12,
"eq" : -1,
"aux" : 0,
"replacementContext" : "λx x = v0 / K(v2, v1) * K(v2, v1) * (1 * (v0 / K(v2, v1) * K(v2, v1)))"
},
"14" : {
"name" : "CutRule",
"leftSubProof" : 10,
"aux1" : 0,
"rightSubProof" : 13,
"aux2" : -1
},
"15" : {
"name" : "WeakeningLeftRule",
"subProof" : 14,
"formula" : "1 * (v0 / K(v2, v1) * K(v2, v1)) = v0 / K(v2, v1) * K(v2, v1)"
},
"16" : {
"name" : "EqualityRightRule",
"subProof" : 15,
"eq" : -1,
"aux" : 0,
"replacementContext" : "λx\n v0 / K(v2, v1) * (K(v2, v1) * 1) * (v0 / K(v2, v1)) * K(v2, v1) =\n v0 / K(v2, v1) * K(v2, v1) * x"
},
"17" : {
"name" : "CutRule",
"leftSubProof" : 6,
"aux1" : 0,
"rightSubProof" : 16,
"aux2" : -1
},
"18" : {
"name" : "WeakeningLeftRule",
"subProof" : 17,
"formula" : "K(v2, v1) * 1 = K(v2, v1)"
},
"19" : {
"name" : "EqualityRightRule",
"subProof" : 18,
"eq" : -1,
"aux" : 0,
"replacementContext" : "λx\n v0 / K(v2, v1) * x * (v0 / K(v2, v1)) * K(v2, v1) =\n v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1) * K(v2, v1))"
},
"20" : {
"name" : "CutRule",
"leftSubProof" : 4,
"aux1" : 0,
"rightSubProof" : 19,
"aux2" : -1
},
"21" : {
"name" : "LogicalAxiom",
"A" : "'\\\\'(v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1)),\n v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1) * K(v2, v1))) =\n L(K(v2, v1), v0 / K(v2, v1), v0 / K(v2, v1) * K(v2, v1))"
},
"22" : {
"name" : "ForallLeftRule",
"subProof" : 21,
"aux" : -1,
"A" : "'\\\\'(v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1)),\n v0 / K(v2, v1) * K(v2, v1) * (v0 / K(v2, v1) * v2_0)) =\n L(v2_0, v0 / K(v2, v1), v0 / K(v2, v1) * K(v2, v1))",
"term" : "K(v2, v1)",
"v" : "v2
```

Seems like there is a limit :/

I'll send by e-mail to those who need

Each file appears 4 times in those numbers.

Out of the 'ok' ones this is the mode breakdown:

```
mode
analytic_independent 17
analytic_sequential 39
spind 6
treegrammar 6
```

It is surprising to me that spind is significantly worse that analytic_sequential and analytic_indepedent.

It should be possible to be as good as / better than these without having to invest too much effort.

@jannikvierling Do you have some documentation about the analytic induction axioms that you could send Andreas?

@andreasfrom what does return status "failed" mean? I assume that "ok" means a proof has been found.