[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
Manuel Eberl
eberlm at in.tum.de
Sun Sep 2 16:00:25 CEST 2018
Okay I did some more experiments and I was now, interestingly enough,
completely unable to reproduce the situation where Green /didn't/
timeout. So I have no idea what was going on there; perhaps I made a
mistake in testing it. I don't know.
It might be wise to remove "continuous_on_discrete" etc. from
intro/continuous_intros and declare it as a simp rule instead. I'm still
not quite sure what causes these problems. I attached a log of blast
with "blast_trace" enabled.
Manuel
On 01/09/2018 14:20, Makarius wrote:
> This thread consists of two sub-threads. The hardware / OS question
> still needs to be sorted out: it might be something with Arch Linux.
>
> Apart from that, my reading of blast.ML is that the "continuous_on" rule
> is applied in the search independently of its fine-grained type
> information. Is that correct?
>
>
> Makarius
>
>
> On 01/09/18 13:19, Lawrence Paulson wrote:
>> Surely the main issue that blast somehow behaves differently depending upon which machine it’s running on?
>>
>> Larry
>>
>>> On 31 Aug 2018, at 22:35, Makarius <makarius at sketis.net> wrote:
>>>
>>> On 31/08/18 22:00, Manuel Eberl wrote:
>>>> That's interesting. I suspected one of the "continuous_on" rules would
>>>> be the cause. In any case, I don't know how the unification works
>>>> exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
>>>> apply to this goal at all due to its restrictive type class constraint.
>>> Blast does its own unification, without taking fully account of types
>>> and type classes. The found proof is then reconstructed as in "fast" and
>>> its friends, using regular Isabelle term + type unification.
>>>
>>> Larry should be able to say more precisely, what the limits of blast are.
-------------- next part --------------
[0]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[0]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
[1]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[1]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[1]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
branch closed by rule
(duplicating)
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
moving formula to unsafe list
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
[2]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[2]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[2]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
branch closed by rule
(duplicating)
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
moving formula to unsafe list
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[1]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[1]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[1]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Excessive branching: KILLED
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
[3]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[3]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[3]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
branch closed by rule
(duplicating)
[3]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
moving formula to unsafe list
[3]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[2]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[2]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[2]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[1]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[1]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[1]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Excessive branching: KILLED
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[2]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[1]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[1]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[1]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Excessive branching: KILLED
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[2]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[1]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[1]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
set ?var
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch closed by rule
1 variable UPDATED:
bot
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[1]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Excessive branching: KILLED
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
[2]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Excessive branching: KILLED
+
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[1]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[1]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[1]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch closed by rule
1 variable UPDATED:
bot
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 3 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
[1]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Excessive branching: KILLED
+
+
[1]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
+
+
[0]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
+
+
[0]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
+
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
+
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 4 branches
branch closed by rule
1 variable UPDATED:
set ?var
+
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - set ?var :: bool ⇒ bool
moving formula to literals
+
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 4 branches
branch closed by rule
1 variable UPDATED:
bot
+
+
[0]
¬ (λx. (f x, g x)) C1_differentiable_on S - bot :: bool ⇒ bool
moving formula to literals
+
+
[0]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 4 branches
branch extended (1 new subgoal)
1 variable UPDATED:
?var - insert ?var ?var
Excessive branching: KILLED
moving formula to unsafe list
+
+
+
[0]
¬ finite ?var :: bool ⇒ bool (Unsafe)
Limit reached.
Backtracking; now there are 3 branches
Backtracking; now there are 3 branches
Backtracking; now there are 2 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
Backtracking; now there are 2 branches
Backtracking; now there are 1 branches
Backtracking; now there are 1 branches
[4]
¬ (continuous_on S (λx. (f x, g x)) ∧ (∃Sa. finite Sa ∧ (λx. (?etc, ?etc)) C1_differentiable_on S - Sa)) :: bool ⇒ bool
branch split: 2 new subgoals
+
[4]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool
moving formula to unsafe list
+
[4]
¬ continuous_on S (λx. (f x, g x)) :: bool ⇒ bool (Unsafe)
branch closed by rule
(duplicating)
[4]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool
moving formula to unsafe list
[4]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[3]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[3]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[3]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[3]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[2]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
+
[2]
¬ finite ?var :: bool ⇒ bool
branch closed by rule
1 variable UPDATED:
set_mset ?var
[2]
¬ (λx. (f x, g x)) C1_differentiable_on S - set_mset ?var :: bool ⇒ bool
moving formula to literals
[2]
∄Sa. finite Sa ∧ (λx. (f x, g x)) C1_differentiable_on S - Sa :: bool ⇒ bool (Unsafe)
branch extended (1 new subgoal)
(duplicating)
[1]
¬ (finite ?var ∧ (λx. (f x, g x)) C1_differentiable_on S - ?var) :: bool ⇒ bool
branch split: 2 new subgoals
Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pEpkey.asc
Type: application/pgp-keys
Size: 1757 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180902/4bde0449/attachment-0002.key>
More information about the isabelle-dev
mailing list