[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