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 <makar...@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.
[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?
pEpkey.asc
Description: application/pgp-keys
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
