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

- 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
- Jun 07 23:32Jenkins nightly build failure

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.

@jannikvierling Yes, sorry I should have said I did try that, but it didn't seem to make much of a difference, giving me errors directly from the tip tool instead. Here is an example where

`fixupAndLoad`

just gives a different error (because of this, I think):```
scala> val problem = TipSmtImporter.fixupAndLoad("benchmarks/isaplanner/prop_02.smt2")
java.util.NoSuchElementException: None.get
```

Adding axioms one at a time and doing a couple of loops in between improves spind a bit. I think testing axioms before adding them might potentially help a lot. (timeout also increased from 30s to 45s)

```
mode
analytic_independent 17
analytic_sequential 40
spind 15
treegrammar 7
```

I could very well image that testing is quite useful.

It may also be worthwhile to have a closer look at the difference between independent and sequential induction axioms, maybe spind can somehow emulate the use of the sequential induction axioms

@jannikvierling Great, thank you!